set R = the trivial complete strict TopLattice;
take the trivial complete strict TopLattice ; :: thesis: ( the trivial complete strict TopLattice is strict & the trivial complete strict TopLattice is continuous & the trivial complete strict TopLattice is compact & the trivial complete strict TopLattice is Hausdorff & the trivial complete strict TopLattice is Lawson )
thus ( the trivial complete strict TopLattice is strict & the trivial complete strict TopLattice is continuous & the trivial complete strict TopLattice is compact & the trivial complete strict TopLattice is Hausdorff & the trivial complete strict TopLattice is Lawson ) ; :: thesis: verum