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