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