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 } c= bool (ultraset BL)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } ; :: thesis:
then ex B being Subset-Family of (ultraset BL) st
( x = union B & B c= StoneR BL ) ;
hence x in bool (ultraset BL) ; :: thesis:

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 #);
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:
assume x in { F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } ; :: thesis:
then ex F being Filter of BL st
( F = x & F is being_ultrafilter & Top BL in F ) ;
hence x in ultraset BL ; :: thesis:

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 A2, XBOOLE_1:1;
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:
assume x in ultraset BL ; :: thesis:
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:

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:

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:
assume A8: a c= the topology of TopStruct(# (ultraset BL),STP #) ; :: thesis:
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:
assume x in { A where A is Subset of (StoneR BL) : union A in a } ; :: thesis:
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:

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 EQREL_1:54;
A10: a c= { (union A) where A is Subset of (StoneR BL) : A in BS }

proof

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

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:
assume x in { (union A) where A is Subset of (StoneR BL) : A in BS } ; :: thesis:
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:

end;

then A16: a = { (union 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 A9, A16; :: thesis:

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:
assume that
A17: p in the topology of TopStruct(# (ultraset BL),STP #) and
A18: q in the topology of TopStruct(# (ultraset BL),STP #) ; :: thesis:
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 Q) = 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:
assume x in INTERSECTION (P,Q) ; :: thesis:
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 A24, A25, XBOOLE_1:8;
then X /\ Y c= ultraset BL by A27;
hence x in bool (ultraset BL) by A26; :: thesis:

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:
assume x in C ; :: thesis:
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 A20, A28, Th23;
consider b being Element of BL such that
A32: Y = (UFilter BL) . b by A22, A29, Th23;
A33: X = { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } by A31, Def6;
A34: Y = { F where F is Filter of BL : ( F is being_ultrafilter & b in F ) } by A32, Def6;
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:
assume A37: x in X /\ Y ; :: thesis:
then A38: x in X by XBOOLE_0:def 4;
A39: x in Y by A37, XBOOLE_0:def 4;
consider F1 being Filter of BL such that
A40: x = F1 and
A41: F1 is being_ultrafilter and
A42: a in F1 by A33, A38;
ex F2 being Filter of BL st
( x = F2 & F2 is being_ultrafilter & b in F2 ) by A34, A39;
then a "/\" b in F1 by A40, A42, FILTER_0:8;
hence x in { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } by A40, A41; :: thesis:

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:
assume x in { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } ; :: thesis:
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 A45, FILTER_0:8;
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 A33, A47, A48;
b in F0 by A45, FILTER_0:8;
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 A34, A51, A52;
hence x in X /\ Y by A43, A46, A49, A50, XBOOLE_0:def 4; :: thesis:

end;

hence X /\ Y = { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } by A36; :: thesis:

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 A30, A35, Th23; :: thesis:

end;

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

end;

hence TopStruct(# (ultraset BL),STP #) is strict TopSpace by A1, A7, PRE_TOPC:def 1; :: thesis:

end;

then reconsider TS = TopStruct(# (ultraset BL),STP #) as strict TopSpace ;
take TS ; :: thesis:
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: