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)

TopStruct(# (ultraset BL),STP #) is 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

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

then reconsider STP = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } as Subset-Family of (ultraset BL) ;
let x be object ; :: 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 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;assume x in { (union A) 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

TopStruct(# (ultraset BL),STP #) is strict TopSpace

proof

then reconsider TS = TopStruct(# (ultraset BL),STP #) as strict TopSpace ;
set TS = TopStruct(# (ultraset BL),STP #);

A1: the carrier of TopStruct(# (ultraset BL),STP #) in the topology of TopStruct(# (ultraset BL),STP #)

union a in the topology of TopStruct(# (ultraset BL),STP #)

p /\ q in the topology of TopStruct(# (ultraset BL),STP #)

end;A1: the carrier of TopStruct(# (ultraset BL),STP #) in the topology of TopStruct(# (ultraset BL),STP #)

proof

A7:
for a being Subset-Family of TopStruct(# (ultraset BL),STP #) st a c= the topology of TopStruct(# (ultraset BL),STP #) holds
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

{ { 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 ) }

(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;{ F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F ) } c= ultraset BL

proof

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

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

then A6:
ultraset BL = union SB
by A3;
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;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

(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

union a in the topology of TopStruct(# (ultraset BL),STP #)

proof

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

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 }

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: verum

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

then reconsider BS = { A where A is Subset of (StoneR BL) : union A in a } as Subset-Family of (StoneR BL) ;
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;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

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

{ (union A) where A is Subset of (StoneR BL) : A in BS } c= a
let x be object ; :: 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 A11: 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

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: verum

end;assume A11: 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

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: verum

proof

then A16:
a = { (union A) where A is Subset of (StoneR BL) : A in BS }
by A10;
let x be object ; :: 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 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;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 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

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: verum

p /\ q in the topology of TopStruct(# (ultraset BL),STP #)

proof

hence
TopStruct(# (ultraset BL),STP #) is strict TopSpace
by A1, A7, PRE_TOPC:def 1; :: thesis: verum
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 Q) = union (INTERSECTION (P,Q)) by SETFAM_1:28;

INTERSECTION (P,Q) c= bool (ultraset BL)

reconsider C = C as Subset-Family of (ultraset BL) ;

C c= StoneR BL

end;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 Q) = union (INTERSECTION (P,Q)) by SETFAM_1:28;

INTERSECTION (P,Q) c= bool (ultraset BL)

proof

then reconsider C = INTERSECTION (P,Q) as Subset-Family of (ultraset BL) ;
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 A24, A25, XBOOLE_1:8;

then X /\ Y c= ultraset BL by A27;

hence x in bool (ultraset BL) by A26; :: thesis: verum

end;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 A24, A25, XBOOLE_1:8;

then X /\ Y c= ultraset BL by A27;

hence x in bool (ultraset BL) by A26; :: thesis: verum

reconsider C = C as Subset-Family of (ultraset BL) ;

C c= StoneR BL

proof

hence
p /\ q in the topology of TopStruct(# (ultraset BL),STP #)
by A19, A21, A23; :: thesis: verum
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 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 ) }

hence x in StoneR BL by A30, A35, Th23; :: thesis: verum

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

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

end;proof

{ F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) } c= X /\ Y
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 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: verum

end;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 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: verum

proof

hence
X /\ Y = { F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F ) }
by A36; :: thesis: verum
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 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: verum

end;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 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: verum

hence x in StoneR BL by A30, A35, Th23; :: thesis: verum

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