let L be complete LATTICE; :: thesis: lambda L c= xi L
consider T being correct Lawson TopAugmentation of L;
consider S being Scott TopAugmentation of L;
consider LL being correct lower TopAugmentation of L;
consider LI being lim-inf TopAugmentation of L;
A1: lambda L = the topology of T by WAYBEL19:def 4;
A2: sigma L = the topology of S by YELLOW_9:51;
A3: omega L = the topology of LL by WAYBEL19:def 2;
A4: xi L = the topology of LI by Th10;
A5: ( RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of L,the InternalRel of L #) & RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of L,the InternalRel of L #) & RelStr(# the carrier of LL,the InternalRel of LL #) = RelStr(# the carrier of L,the InternalRel of L #) & RelStr(# the carrier of LI,the InternalRel of LI #) = RelStr(# the carrier of L,the InternalRel of L #) ) by YELLOW_9:def 4;
A6: T is Refinement of S,LL by WAYBEL19:29;
( the topology of S c= xi L & the topology of LL c= xi L ) by A2, A3, Th19, Th21;
then ( LI is TopExtension of S & LI is TopExtension of LL ) by A4, A5, YELLOW_9:def 5;
then LI is TopExtension of T by A6, Th22;
hence lambda L c= xi L by A1, A4, YELLOW_9:def 5; :: thesis: verum