consider T being trivial complete strict TopLattice;
take T ; :: thesis: ( T is lower & T is trivial & T is complete & T is strict )
thus ( T is lower & T is trivial & T is complete & T is strict ) ; :: thesis: verum