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: RelStr(# the carrier of LI,the InternalRel of LI #) = RelStr(# the carrier of L,the InternalRel of L #) by YELLOW_9:def 4;
A2: xi L = the topology of LI by Th10;
omega L = the topology of LL by WAYBEL19:def 2;
then ( RelStr(# the carrier of LL,the InternalRel of LL #) = RelStr(# the carrier of L,the InternalRel of L #) & the topology of LL c= xi L ) by Th21, YELLOW_9:def 4;
then A3: LI is TopExtension of LL by A2, A1, YELLOW_9:def 5;
sigma L = the topology of S by YELLOW_9:51;
then ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of L,the InternalRel of L #) & the topology of S c= xi L ) by Th19, YELLOW_9:def 4;
then ( T is Refinement of S,LL & LI is TopExtension of S ) by A2, A1, WAYBEL19:29, YELLOW_9:def 5;
then ( lambda L = the topology of T & LI is TopExtension of T ) by A3, Th22, WAYBEL19:def 4;
hence lambda L c= xi L by A2, YELLOW_9:def 5; :: thesis: verum