...theory.

The Mizar proof checker accepts the definitions essentially as they are, but the first proof in Mizar is 400 lines.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.