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