set US = ultraset BL;
set STP = { () where A is Subset-Family of (ultraset BL) : A c= StoneR BL } ;
{ (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } c= bool (ultraset BL)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { () where A is Subset-Family of (ultraset BL) : A c= StoneR BL } or x in bool (ultraset BL) )
assume x in { () where A is Subset-Family of (ultraset BL) : A c= StoneR BL } ; :: thesis: x in bool (ultraset BL)
then ex B being Subset-Family of (ultraset BL) st
( x = union B & B c= StoneR BL ) ;
hence x in bool (ultraset BL) ; :: thesis: verum
end;
then reconsider STP = { () where A is Subset-Family of (ultraset BL) : A c= StoneR BL } as Subset-Family of (ultraset BL) ;
TopStruct(# (ultraset BL),STP #) is strict TopSpace
proof
set TS = TopStruct(# (ultraset BL),STP #);
A1: the carrier of TopStruct(# (ultraset BL),STP #) in the topology of TopStruct(# (ultraset BL),STP #)
proof
set B = { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } ;
{ F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } c= ultraset BL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } or x in ultraset BL )
assume x in { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } ; :: thesis: x in ultraset BL
then ex F being Filter of BL st
( F = x & F is being_ultrafilter & Top BL in F ) ;
hence x in ultraset BL ; :: thesis: verum
end;
then A2: bool { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } c= bool (ultraset BL) by ZFMISC_1:67;
{ { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } } c= bool { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } by ZFMISC_1:68;
then reconsider SB = { { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } } as Subset-Family of (ultraset BL) by ;
reconsider SB = SB as Subset-Family of (ultraset BL) ;
A3: union SB = { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } by ZFMISC_1:25;
ultraset BL c= { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ultraset BL or x in { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } )
assume x in ultraset BL ; :: thesis: x in { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) }
then consider F being Filter of BL such that
A4: F = x and
A5: F is being_ultrafilter ;
Top BL in F by FILTER_0:11;
hence x in { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } by A4, A5; :: thesis: verum
end;
then A6: ultraset BL = union SB by A3;
(UFilter BL) . (Top BL) = { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } by Def6;
then { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } in StoneR BL by Th23;
then SB c= StoneR BL by ZFMISC_1:31;
hence the carrier of TopStruct(# (ultraset BL),STP #) in the topology of TopStruct(# (ultraset BL),STP #) by A6; :: thesis: verum
end;
A7: for a being Subset-Family of TopStruct(# (ultraset BL),STP #) st a c= the topology of TopStruct(# (ultraset BL),STP #) holds
union a in the topology of TopStruct(# (ultraset BL),STP #)
proof
let a be Subset-Family of TopStruct(# (ultraset BL),STP #); :: thesis: ( a c= the topology of TopStruct(# (ultraset BL),STP #) implies union a in the topology of TopStruct(# (ultraset BL),STP #) )
assume A8: a c= the topology of TopStruct(# (ultraset BL),STP #) ; :: thesis: union a in the topology of TopStruct(# (ultraset BL),STP #)
set B = { A where A is Subset of (StoneR BL) : union A in a } ;
{ A where A is Subset of (StoneR BL) : union A in a } c= bool (StoneR BL)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of (StoneR BL) : union A in a } or x in bool (StoneR BL) )
assume x in { A where A is Subset of (StoneR BL) : union A in a } ; :: thesis: x in bool (StoneR BL)
then ex C being Subset of (StoneR BL) st
( C = x & union C in a ) ;
then reconsider C = x as Subset of (StoneR BL) ;
C c= StoneR BL ;
hence x in bool (StoneR BL) ; :: thesis: verum
end;
then reconsider BS = { A where A is Subset of (StoneR BL) : union A in a } as Subset-Family of (StoneR BL) ;
A9: union (union BS) = union { () where A is Subset of (StoneR BL) : A in BS } by EQREL_1:54;
A10: a c= { () where A is Subset of (StoneR BL) : A in BS }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a or x in { () where A is Subset of (StoneR BL) : A in BS } )
assume A11: x in a ; :: thesis: x in { () where A is Subset of (StoneR BL) : A in BS }
then x in STP by A8;
then consider C being Subset-Family of (ultraset BL) such that
A12: x = union C and
A13: C c= StoneR BL ;
C in BS by ;
hence x in { () where A is Subset of (StoneR BL) : A in BS } by A12; :: thesis: verum
end;
{ (union A) where A is Subset of (StoneR BL) : A in BS } c= a
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { () where A is Subset of (StoneR BL) : A in BS } or x in a )
assume x in { () where A is Subset of (StoneR BL) : A in BS } ; :: thesis: x in a
then consider C being Subset of (StoneR BL) such that
A14: union C = x and
A15: C in BS ;
ex D being Subset of (StoneR BL) st
( D = C & union D in a ) by A15;
hence x in a by A14; :: thesis: verum
end;
then A16: a = { () where A is Subset of (StoneR BL) : A in BS } by A10;
union BS is Subset-Family of (ultraset BL) by XBOOLE_1:1;
hence union a in the topology of TopStruct(# (ultraset BL),STP #) by ; :: thesis: verum
end;
for p, q being Subset of TopStruct(# (ultraset BL),STP #) st p in the topology of TopStruct(# (ultraset BL),STP #) & q in the topology of TopStruct(# (ultraset BL),STP #) holds
p /\ q in the topology of TopStruct(# (ultraset BL),STP #)
proof
let p, q be Subset of TopStruct(# (ultraset BL),STP #); :: thesis: ( p in the topology of TopStruct(# (ultraset BL),STP #) & q in the topology of TopStruct(# (ultraset BL),STP #) implies p /\ q in the topology of TopStruct(# (ultraset BL),STP #) )
assume that
A17: p in the topology of TopStruct(# (ultraset BL),STP #) and
A18: q in the topology of TopStruct(# (ultraset BL),STP #) ; :: thesis: p /\ q in the topology of TopStruct(# (ultraset BL),STP #)
consider P being Subset-Family of (ultraset BL) such that
A19: union P = p and
A20: P c= StoneR BL by A17;
consider Q being Subset-Family of (ultraset BL) such that
A21: union Q = q and
A22: Q c= StoneR BL by A18;
A23: (union P) /\ () = union (INTERSECTION (P,Q)) by SETFAM_1:28;
INTERSECTION (P,Q) c= bool (ultraset BL)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in INTERSECTION (P,Q) or x in bool (ultraset BL) )
assume x in INTERSECTION (P,Q) ; :: thesis: x in bool (ultraset BL)
then consider X, Y being set such that
A24: X in P and
A25: Y in Q and
A26: x = X /\ Y by SETFAM_1:def 5;
A27: X /\ Y c= X \/ Y by XBOOLE_1:29;
X \/ Y c= ultraset BL by ;
then X /\ Y c= ultraset BL by A27;
hence x in bool (ultraset BL) by A26; :: thesis: verum
end;
then reconsider C = INTERSECTION (P,Q) as Subset-Family of (ultraset BL) ;
reconsider C = C as Subset-Family of (ultraset BL) ;
C c= StoneR BL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in StoneR BL )
assume x in C ; :: thesis: x in StoneR BL
then consider X, Y being set such that
A28: X in P and
A29: Y in Q and
A30: x = X /\ Y by SETFAM_1:def 5;
consider a being Element of BL such that
A31: X = (UFilter BL) . a by ;
consider b being Element of BL such that
A32: Y = (UFilter BL) . b by ;
A33: X = { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } by ;
A34: Y = { F where F is Filter of BL : ( F is being_ultrafilter & b in F ) } by ;
A35: X /\ Y = { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) }
proof
A36: X /\ Y c= { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ Y or x in { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } )
assume A37: x in X /\ Y ; :: thesis: x in { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) }
then A38: x in X by XBOOLE_0:def 4;
A39: x in Y by ;
consider F1 being Filter of BL such that
A40: x = F1 and
A41: F1 is being_ultrafilter and
A42: a in F1 by ;
ex F2 being Filter of BL st
( x = F2 & F2 is being_ultrafilter & b in F2 ) by ;
then a "/\" b in F1 by ;
hence x in { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } by ; :: thesis: verum
end;
{ F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } c= X /\ Y
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } or x in X /\ Y )
assume x in { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } ; :: thesis: x in X /\ Y
then consider F0 being Filter of BL such that
A43: x = F0 and
A44: F0 is being_ultrafilter and
A45: a "/\" b in F0 ;
a in F0 by ;
then consider F being Filter of BL such that
A46: F = F0 and
A47: F is being_ultrafilter and
A48: a in F by A44;
A49: F in X by ;
b in F0 by ;
then consider F1 being Filter of BL such that
A50: F1 = F0 and
A51: F1 is being_ultrafilter and
A52: b in F1 by A44;
F1 in Y by ;
hence x in X /\ Y by ; :: thesis: verum
end;
hence X /\ Y = { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } by A36; :: thesis: verum
end;
(UFilter BL) . (a "/\" b) = { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } by Def6;
hence x in StoneR BL by ; :: thesis: verum
end;
hence p /\ q in the topology of TopStruct(# (ultraset BL),STP #) by ; :: thesis: verum
end;
hence TopStruct(# (ultraset BL),STP #) is strict TopSpace by ; :: thesis: verum
end;
then reconsider TS = TopStruct(# (ultraset BL),STP #) as strict TopSpace ;
take TS ; :: thesis: ( the carrier of TS = ultraset BL & the topology of TS = { () where A is Subset-Family of (ultraset BL) : A c= StoneR BL } )
thus ( the carrier of TS = ultraset BL & the topology of TS = { () where A is Subset-Family of (ultraset BL) : A c= StoneR BL } ) ; :: thesis: verum