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