set L = the non empty trivial TopLattice;
take the non empty trivial TopLattice ; :: thesis: ( the non empty trivial TopLattice is lim-inf & the non empty trivial TopLattice is continuous & the non empty trivial TopLattice is complete )
thus ( the non empty trivial TopLattice is lim-inf & the non empty trivial TopLattice is continuous & the non empty trivial TopLattice is complete ) ; :: thesis: verum