set A = the trivial strict TopLattice;
take the trivial strict TopLattice ; :: thesis: ( the trivial strict TopLattice is strict & the trivial strict TopLattice is continuous & the trivial strict TopLattice is lower-bounded & the trivial strict TopLattice is meet-continuous & the trivial strict TopLattice is Scott )
thus ( the trivial strict TopLattice is strict & the trivial strict TopLattice is continuous & the trivial strict TopLattice is lower-bounded & the trivial strict TopLattice is meet-continuous & the trivial strict TopLattice is Scott ) ; :: thesis: verum