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