let L be complete LATTICE; :: thesis: omega L c= xi L
set S = the correct lower TopAugmentation of L;
set X = the lim-inf TopAugmentation of L;
reconsider B = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of L : verum } as prebasis of the correct lower TopAugmentation of L by WAYBEL19:def 1;
A1: ( 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 #) & 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: B c= the topology of the lim-inf TopAugmentation of L

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in B or b in the topology of the lim-inf TopAugmentation of L )
assume b in B ; :: thesis: b in the topology of the lim-inf TopAugmentation of L
then consider x being Element of the correct lower TopAugmentation of L such that
A3: b = (uparrow x) ` ;
reconsider y = x as Element of the lim-inf TopAugmentation of L by A1;
set A = uparrow y;
the lim-inf TopAugmentation of L is SubRelStr of the lim-inf TopAugmentation of L by YELLOW_6:6;
then the correct lower TopAugmentation of L is SubRelStr of the lim-inf TopAugmentation of L by A1, WAYBEL21:12;
then A4: uparrow x c= uparrow y by WAYBEL23:14;
A5: inf (uparrow y) = y by WAYBEL_0:39;

now :: thesis: for F being ultra Filter of (BoolePoset ([#] the lim-inf TopAugmentation of L)) st uparrow y in F holds
lim_inf F in uparrow y

let F be ultra Filter of (BoolePoset ([#] the lim-inf TopAugmentation of L)); :: thesis: ( uparrow y in F implies lim_inf F in uparrow y )
assume uparrow y in F ; :: thesis: lim_inf F in uparrow y
then inf (uparrow y) in { (inf C) where C is Subset of the lim-inf TopAugmentation of L : C in F } ;
then inf (uparrow y) <= "\/" ( { (inf C) where C is Subset of the lim-inf TopAugmentation of L : C in F } , the lim-inf TopAugmentation of L) by YELLOW_2:22;
hence lim_inf F in uparrow y by A5, WAYBEL_0:18; :: thesis: verum

end;

then A6: uparrow y is closed by Th18;
the correct lower TopAugmentation of L is SubRelStr of the correct lower TopAugmentation of L by YELLOW_6:6;
then the lim-inf TopAugmentation of L is SubRelStr of the correct lower TopAugmentation of L by A1, WAYBEL21:12;
then uparrow y c= uparrow x by WAYBEL23:14;
then uparrow y = uparrow x by A4;
hence b in the topology of the lim-inf TopAugmentation of L by A1, A3, A6, PRE_TOPC:def 2; :: thesis: verum

end;

the carrier of the correct lower TopAugmentation of L in the topology of the lim-inf TopAugmentation of L by A1, PRE_TOPC:def 1;
then the topology of the correct lower TopAugmentation of L c= the topology of the lim-inf TopAugmentation of L by A2, Th20;
then omega L c= the topology of the lim-inf TopAugmentation of L by WAYBEL19:def 2;
hence omega L c= xi L by Th10; :: thesis: verum