let T be complete TopLattice; :: thesis: ( T is trivial implies T is Lawson )
assume T is trivial ; :: thesis: T is Lawson
then reconsider W = T as trivial complete TopLattice ;
A1: the topology of W = {{} ,the carrier of W} by TDLAT_3:def 2;
consider N being correct Lawson TopAugmentation of W;
RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of N,the InternalRel of N #) by YELLOW_9:def 4;
then the topology of T = the topology of N by A1, TDLAT_3:def 2
.= lambda T by WAYBEL19:def 4
.= UniCl (FinMeetCl ((sigma T) \/ (omega T))) by WAYBEL19:33 ;
then FinMeetCl ((omega T) \/ (sigma T)) is Basis of T by YELLOW_9:22;
hence (omega T) \/ (sigma T) is prebasis of T by YELLOW_9:23; :: according to WAYBEL19:def 3 :: thesis: verum