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

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