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

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

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

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;
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;

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;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

then A6:
uparrow y is closed
by Th18;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;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

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

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