let L be complete LATTICE; :: thesis: omega L c= xi L
consider S being correct lower TopAugmentation of L;
consider X being lim-inf TopAugmentation of L;
A1: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of L,the InternalRel of L #) & RelStr(# the carrier of X,the InternalRel of X #) = RelStr(# the carrier of L,the InternalRel of L #) ) by YELLOW_9:def 4;
reconsider B = { ((uparrow x) ` ) where x is Element of S : verum } as prebasis of S by WAYBEL19:def 1;
A2: the carrier of S in the topology of X by A1, PRE_TOPC:def 1;
B c= the topology of X

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in B or b in the topology of X )
assume b in B ; :: thesis: b in the topology of X
then consider x being Element of S such that
A3: b = (uparrow x) ` ;
reconsider y = x as Element of X by A1;
S is SubRelStr of S by YELLOW_6:15;
then X is SubRelStr of S by A1, WAYBEL21:12;
then A4: uparrow y c= uparrow x by WAYBEL23:14;
X is SubRelStr of X by YELLOW_6:15;
then S is SubRelStr of X by A1, WAYBEL21:12;
then uparrow x c= uparrow y by WAYBEL23:14;
then A5: uparrow y = uparrow x by A4, XBOOLE_0:def 10;
set A = uparrow y;
A6: inf (uparrow y) = y by WAYBEL_0:39;

now

let F be ultra Filter of (BoolePoset ([#] X)); :: 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 X : C in F } ;
then inf (uparrow y) <= "\/" { (inf C) where C is Subset of X : C in F } ,X by YELLOW_2:24;
hence lim_inf F in uparrow y by A6, WAYBEL_0:18; :: thesis: verum

end;

then uparrow y is closed by Th18;
then (uparrow y) ` is open ;
hence b in the topology of X by A1, A3, A5, PRE_TOPC:def 5; :: thesis: verum

end;

then the topology of S c= the topology of X by A2, Th20;
then omega L c= the topology of X by WAYBEL19:def 2;
hence omega L c= xi L by Th10; :: thesis: verum