set
L
= the
strict
complete
LATTICE
;
take
the
strict
complete
LATTICE
;
:: thesis:
( the
strict
complete
LATTICE
is
complete
& the
strict
complete
LATTICE
is
strict
)
thus
( the
strict
complete
LATTICE
is
complete
& the
strict
complete
LATTICE
is
strict
) ;
:: thesis:
verum