let T be complete TopLattice; :: thesis: ( T is trivial implies T is Lawson )
assume T is trivial ; :: thesis: T is Lawson
then the carrier of T is 1 -element ;
then reconsider W = T as 1 -element complete TopLattice by STRUCT_0:def 19;
set N = the correct Lawson TopAugmentation of W;
A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of the correct Lawson TopAugmentation of W, the InternalRel of the correct Lawson TopAugmentation of W #) by YELLOW_9:def 4;
the topology of W = {{}, the carrier of W} by TDLAT_3:def 2;
then the topology of T = the topology of the correct Lawson TopAugmentation of W 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