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

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