set US = PFilters L;
set STP = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } ;
{ (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } c= bool (PFilters L)

proof

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

end;

then reconsider STP = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } as Subset-Family of (PFilters L) ;
TopStruct(# (PFilters L),STP #) is strict TopSpace

proof

set TS = TopStruct(# (PFilters L),STP #);
A1: the carrier of TopStruct(# (PFilters L),STP #) in the topology of TopStruct(# (PFilters L),STP #)

proof

set B = { F where F is Filter of L : ( F is prime & Top L in F ) } ;
{ F where F is Filter of L : ( F is prime & Top L in F ) } c= PFilters L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Filter of L : ( F is prime & Top L in F ) } or x in PFilters L )
assume x in { F where F is Filter of L : ( F is prime & Top L in F ) } ; :: thesis: x in PFilters L
then ex F being Filter of L st
( F = x & F is prime & Top L in F ) ;
hence x in PFilters L ; :: thesis: verum

end;

then A2: bool { F where F is Filter of L : ( F is prime & Top L in F ) } c= bool (PFilters L) by ZFMISC_1:67;
{ { F where F is Filter of L : ( F is prime & Top L in F ) } } c= bool { F where F is Filter of L : ( F is prime & Top L in F ) } by ZFMISC_1:68;
then reconsider SB = { { F where F is Filter of L : ( F is prime & Top L in F ) } } as Subset-Family of (PFilters L) by A2, XBOOLE_1:1;
reconsider SB = SB as Subset-Family of (PFilters L) ;
PFilters L c= { F where F is Filter of L : ( F is prime & Top L in F ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PFilters L or x in { F where F is Filter of L : ( F is prime & Top L in F ) } )
assume x in PFilters L ; :: thesis: x in { F where F is Filter of L : ( F is prime & Top L in F ) }
then consider F being Filter of L such that
A4: F = x and
A5: F is prime ;
Top L in F by FILTER_0:11;
hence x in { F where F is Filter of L : ( F is prime & Top L in F ) } by A4, A5; :: thesis: verum

end;

then A6: PFilters L = union SB by ZFMISC_1:25;
(PrimeFilters L) . (Top L) = { F where F is Filter of L : ( F is prime & Top L in F ) } by Def6;
then SB c= StoneR L by ZFMISC_1:31, Th23;
hence the carrier of TopStruct(# (PFilters L),STP #) in the topology of TopStruct(# (PFilters L),STP #) by A6; :: thesis: verum

end;

A7: for a being Subset-Family of TopStruct(# (PFilters L),STP #) st a c= the topology of TopStruct(# (PFilters L),STP #) holds
union a in the topology of TopStruct(# (PFilters L),STP #)

proof

let a be Subset-Family of TopStruct(# (PFilters L),STP #); :: thesis: ( a c= the topology of TopStruct(# (PFilters L),STP #) implies union a in the topology of TopStruct(# (PFilters L),STP #) )
assume A8: a c= the topology of TopStruct(# (PFilters L),STP #) ; :: thesis: union a in the topology of TopStruct(# (PFilters L),STP #)
set B = { A where A is Subset of (StoneR L) : union A in a } ;
{ A where A is Subset of (StoneR L) : union A in a } c= bool (StoneR L)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of (StoneR L) : union A in a } or x in bool (StoneR L) )
assume x in { A where A is Subset of (StoneR L) : union A in a } ; :: thesis: x in bool (StoneR L)
then ex C being Subset of (StoneR L) st
( C = x & union C in a ) ;
then reconsider C = x as Subset of (StoneR L) ;
C c= StoneR L ;
hence x in bool (StoneR L) ; :: thesis: verum

end;

then reconsider BS = { A where A is Subset of (StoneR L) : union A in a } as Subset-Family of (StoneR L) ;
A9: union (union BS) = union { (union A) where A is Subset of (StoneR L) : A in BS } by EQREL_1:54;
A10: a c= { (union A) where A is Subset of (StoneR L) : A in BS }

proof

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 L) : A in BS } )
assume A11: x in a ; :: thesis: x in { (union A) where A is Subset of (StoneR L) : A in BS }
then x in STP by A8;
then consider C being Subset-Family of (PFilters L) such that
A12: x = union C and
A13: C c= StoneR L ;
C in BS by A11, A12, A13;
hence x in { (union A) where A is Subset of (StoneR L) : A in BS } by A12; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (union A) where A is Subset of (StoneR L) : A in BS } or x in a )
assume x in { (union A) where A is Subset of (StoneR L) : A in BS } ; :: thesis: x in a
then consider C being Subset of (StoneR L) such that
A14: union C = x and
A15: C in BS ;
ex D being Subset of (StoneR L) st
( D = C & union D in a ) by A15;
hence x in a by A14; :: thesis: verum

end;

then A16: a = { (union A) where A is Subset of (StoneR L) : A in BS } by A10;
union BS is Subset-Family of (PFilters L) by XBOOLE_1:1;
hence union a in the topology of TopStruct(# (PFilters L),STP #) by A9, A16; :: thesis: verum

end;

for p, q being Subset of TopStruct(# (PFilters L),STP #) st p in the topology of TopStruct(# (PFilters L),STP #) & q in the topology of TopStruct(# (PFilters L),STP #) holds
p /\ q in the topology of TopStruct(# (PFilters L),STP #)

proof

let p, q be Subset of TopStruct(# (PFilters L),STP #); :: thesis: ( p in the topology of TopStruct(# (PFilters L),STP #) & q in the topology of TopStruct(# (PFilters L),STP #) implies p /\ q in the topology of TopStruct(# (PFilters L),STP #) )
assume that
A17: p in the topology of TopStruct(# (PFilters L),STP #) and
A18: q in the topology of TopStruct(# (PFilters L),STP #) ; :: thesis: p /\ q in the topology of TopStruct(# (PFilters L),STP #)
consider P being Subset-Family of (PFilters L) such that
A19: union P = p and
A20: P c= StoneR L by A17;
consider Q being Subset-Family of (PFilters L) such that
A21: union Q = q and
A22: Q c= StoneR L by A18;
A23: (union P) /\ (union Q) = union (INTERSECTION (P,Q)) by SETFAM_1:28;
INTERSECTION (P,Q) c= bool (PFilters L)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in INTERSECTION (P,Q) or x in bool (PFilters L) )
assume x in INTERSECTION (P,Q) ; :: thesis: x in bool (PFilters L)
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= PFilters L by A24, A25, XBOOLE_1:8;
then X /\ Y c= PFilters L by A27;
hence x in bool (PFilters L) by A26; :: thesis: verum

end;

then reconsider C = INTERSECTION (P,Q) as Subset-Family of (PFilters L) ;
reconsider C = C as Subset-Family of (PFilters L) ;
C c= StoneR L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in StoneR L )
assume x in C ; :: thesis: x in StoneR L
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 L such that
A31: X = (PrimeFilters L) . a by A20, A28, Th23;
consider b being Element of L such that
A32: Y = (PrimeFilters L) . b by A22, A29, Th23;
A33: X = { F where F is Filter of L : ( F is prime & a in F ) } by A31, Def6;
A34: Y = { F where F is Filter of L : ( F is prime & b in F ) } by A32, Def6;
A35: X /\ Y = { F where F is Filter of L : ( F is prime & a "/\" b in F ) }

proof

A36: X /\ Y c= { F where F is Filter of L : ( F is prime & 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 L : ( F is prime & a "/\" b in F ) } )
assume A37: x in X /\ Y ; :: thesis: x in { F where F is Filter of L : ( F is prime & 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 L such that
A40: x = F1 and
A41: F1 is prime and
A42: a in F1 by A33, A38;
ex F2 being Filter of L st
( x = F2 & F2 is prime & 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 L : ( F is prime & a "/\" b in F ) } by A40, A41; :: thesis: verum

end;

{ F where F is Filter of L : ( F is prime & 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 L : ( F is prime & a "/\" b in F ) } or x in X /\ Y )
assume x in { F where F is Filter of L : ( F is prime & a "/\" b in F ) } ; :: thesis: x in X /\ Y
then consider F0 being Filter of L such that
A43: x = F0 and
A44: F0 is prime and
A45: a "/\" b in F0 ;
a in F0 by A45, FILTER_0:8;
then consider F being Filter of L such that
A46: F = F0 and
A47: F is prime 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 L such that
A50: F1 = F0 and
A51: F1 is prime 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;

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

end;

(PrimeFilters L) . (a "/\" b) = { F where F is Filter of L : ( F is prime & a "/\" b in F ) } by Def6;
hence x in StoneR L by A30, A35, Th23; :: thesis: verum

end;

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

end;

hence TopStruct(# (PFilters L),STP #) is strict TopSpace by A1, A7, PRE_TOPC:def 1; :: thesis: verum

end;

then reconsider TS = TopStruct(# (PFilters L),STP #) as strict TopSpace ;
take TS ; :: thesis: ( the carrier of TS = PFilters L & the topology of TS = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } )
thus ( the carrier of TS = PFilters L & the topology of TS = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } ) ; :: thesis: verum