set A = 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 continuous & the 1 -element strict TopLattice is lower-bounded & the 1 -element strict TopLattice is meet-continuous & the 1 -element strict TopLattice is Scott )
thus ( the 1 -element strict TopLattice is strict & the 1 -element strict TopLattice is continuous & the 1 -element strict TopLattice is lower-bounded & the 1 -element strict TopLattice is meet-continuous & the 1 -element strict TopLattice is Scott ) ; :: thesis: verum