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