set T = the trivial complete strict TopLattice;
take the trivial complete strict TopLattice ; :: thesis: ( the trivial complete strict TopLattice is lower & the trivial complete strict TopLattice is trivial & the trivial complete strict TopLattice is complete & the trivial complete strict TopLattice is strict )
thus ( the trivial complete strict TopLattice is lower & the trivial complete strict TopLattice is trivial & the trivial complete strict TopLattice is complete & the trivial complete strict TopLattice is strict ) ; :: thesis: verum