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