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

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