let L be complete LATTICE; :: thesis:
set S = the correct lower TopAugmentation of L;
set X = the lim-inf TopAugmentation of L;
reconsider B = { (() `) 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 = () ` ;
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 ;
then A4: uparrow x c= uparrow y by WAYBEL23:14;
A5: inf () = y by WAYBEL_0:39;
now :: thesis: for F being ultra Filter of (BoolePoset ()) st uparrow y in F holds
lim_inf F in uparrow y
let F be ultra Filter of (BoolePoset ()); :: thesis: ( uparrow y in F implies lim_inf F in uparrow y )
assume uparrow y in F ; :: thesis:
then inf () in { (inf C) where C is Subset of the lim-inf TopAugmentation of L : C in F } ;
then inf () <= "\/" ( { (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 ; :: 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 ;
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 ; :: thesis: verum
end;
the carrier of the correct lower TopAugmentation of L in the topology of the lim-inf TopAugmentation of L by ;
then the topology of the correct lower TopAugmentation of L c= the topology of the lim-inf TopAugmentation of L by ;
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