set US = ultraset BL;
set STP = { (union A) 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 } is Subset-Family of (ultraset BL)

proof

{ (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } c= bool (ultraset BL)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } or x in bool (ultraset BL) )
assume x in { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } ; :: thesis: x in bool (ultraset BL)
then consider B being Subset-Family of (ultraset BL) such that
A1: ( x = union B & B c= StoneR BL ) ;
thus x in bool (ultraset BL) by A1; :: thesis: verum

end;

hence { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } is Subset-Family of (ultraset BL) ; :: thesis: verum

end;

then reconsider STP = { (union A) 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 #);
A2: 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 set ; :: 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 A3: bool { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } c= bool (ultraset BL) by ZFMISC_1:79;
{{ 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:80;
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 A3, XBOOLE_1:1;
reconsider SB = SB as Subset-Family of (ultraset BL) ;
A4: ultraset BL = union SB

proof

A5: union SB = { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } by ZFMISC_1:31;
ultraset BL c= { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) }

proof

let x be set ; :: 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
A6: ( F = x & F is being_ultrafilter ) ;
Top BL in F by FILTER_0:12;
hence x in { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } by A6; :: thesis: verum

end;

hence ultraset BL = union SB by A5, XBOOLE_0:def 10; :: thesis: verum

end;

(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 Th26;
then SB c= StoneR BL by ZFMISC_1:37;
hence the carrier of TopStruct(# (ultraset BL),STP #) in the topology of TopStruct(# (ultraset BL),STP #) by A4; :: 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 set ; :: 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 { (union A) where A is Subset of (StoneR BL) : A in BS } by BORSUK_1:17;
A10: a = { (union A) where A is Subset of (StoneR BL) : A in BS }

proof

A11: a c= { (union A) where A is Subset of (StoneR BL) : A in BS }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in a or x in { (union A) where A is Subset of (StoneR BL) : A in BS } )
assume A12: x in a ; :: thesis: x in { (union A) 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
A13: ( x = union C & C c= StoneR BL ) ;
C in BS by A12, A13;
hence x in { (union A) where A is Subset of (StoneR BL) : A in BS } by A13; :: thesis: verum

end;

{ (union A) where A is Subset of (StoneR BL) : A in BS } c= a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (union A) where A is Subset of (StoneR BL) : A in BS } or x in a )
assume x in { (union A) 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 & C in BS ) ;
consider D being Subset of (StoneR BL) such that
A15: ( D = C & union D in a ) by A14;
thus x in a by A14, A15; :: thesis: verum

end;

hence a = { (union A) where A is Subset of (StoneR BL) : A in BS } by A11, XBOOLE_0:def 10; :: thesis: verum

end;

union BS is Subset-Family of (ultraset BL) by XBOOLE_1:1;
hence union a in the topology of TopStruct(# (ultraset BL),STP #) by A9, A10; :: 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 A16: ( p in the topology of TopStruct(# (ultraset BL),STP #) & q in the topology of TopStruct(# (ultraset BL),STP #) ) ; :: thesis: p /\ q in the topology of TopStruct(# (ultraset BL),STP #)
then consider P being Subset-Family of (ultraset BL) such that
A17: ( union P = p & P c= StoneR BL ) ;
consider Q being Subset-Family of (ultraset BL) such that
A18: ( union Q = q & Q c= StoneR BL ) by A16;
A19: (union P) /\ (union Q) = union (INTERSECTION P,Q) by SETFAM_1:39;
INTERSECTION P,Q c= bool (ultraset BL)

proof

let x be set ; :: 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
A20: ( X in P & Y in Q & x = X /\ Y ) by SETFAM_1:def 5;
A21: X /\ Y c= X \/ Y by XBOOLE_1:29;
X \/ Y c= ultraset BL by A20, XBOOLE_1:8;
then X /\ Y c= ultraset BL by A21, XBOOLE_1:1;
hence x in bool (ultraset BL) by A20; :: 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 set ; :: 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
A22: ( X in P & Y in Q & x = X /\ Y ) by SETFAM_1:def 5;
consider a being Element of BL such that
A23: X = (UFilter BL) . a by A17, A22, Th26;
consider b being Element of BL such that
A24: Y = (UFilter BL) . b by A18, A22, Th26;
A25: X = { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } by A23, Def6;
A26: Y = { F where F is Filter of BL : ( F is being_ultrafilter & b in F ) } by A24, Def6;
A27: X /\ Y = { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) }

proof

A28: X /\ Y c= { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) }

proof

let x be set ; :: 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 x in X /\ Y ; :: thesis: x in { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) }
then A29: ( x in X & x in Y ) by XBOOLE_0:def 4;
then consider F1 being Filter of BL such that
A30: ( x = F1 & F1 is being_ultrafilter & a in F1 ) by A25;
consider F2 being Filter of BL such that
A31: ( x = F2 & F2 is being_ultrafilter & b in F2 ) by A26, A29;
a "/\" b in F1 by A30, A31, FILTER_0:def 1;
then consider F being Filter of BL such that
A32: ( x = F & F is being_ultrafilter & a "/\" b in F ) by A30;
thus x in { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } by A32; :: 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 set ; :: 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
A33: ( x = F0 & F0 is being_ultrafilter & a "/\" b in F0 ) ;
a in F0 by A33, FILTER_0:def 1;
then consider F being Filter of BL such that
A34: ( F = F0 & F is being_ultrafilter & a in F ) by A33;
A35: F in X by A25, A34;
b in F0 by A33, FILTER_0:def 1;
then consider F1 being Filter of BL such that
A36: ( F1 = F0 & F1 is being_ultrafilter & b in F1 ) by A33;
F1 in Y by A26, A36;
hence x in X /\ Y by A33, A34, A35, A36, XBOOLE_0:def 4; :: thesis: verum

end;

hence X /\ Y = { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } by A28, XBOOLE_0:def 10; :: thesis: verum

end;

(UFilter BL) . (a "/\" b) = { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } by Def6;
then consider c being Element of BL such that
A37: ( c = a "/\" b & (UFilter BL) . c = { F where F is Filter of BL : ( F is being_ultrafilter & c in F ) } ) ;
thus x in StoneR BL by A22, A27, A37, Th26; :: thesis: verum

end;

hence p /\ q in the topology of TopStruct(# (ultraset BL),STP #) by A17, A18, A19; :: thesis: verum

end;

hence TopStruct(# (ultraset BL),STP #) is strict TopSpace by A2, A7, PRE_TOPC:def 1; :: 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 = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } )
thus ( the carrier of TS = ultraset BL & the topology of TS = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } ) ; :: thesis: verum