set X = F1();
set F = { A where A is Subset of F1() : P1[A] } ;
{ A where A is Subset of F1() : P1[A] } c= bool F1()
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { A where A is Subset of F1() : P1[A] } or a in bool F1() )
assume a in { A where A is Subset of F1() : P1[A] } ; :: thesis: a in bool F1()
then ex B being Subset of F1() st
( a = B & P1[B] ) ;
hence a in bool F1() ; :: thesis: verum
end;
then reconsider F = { A where A is Subset of F1() : P1[A] } as Subset-Family of F1() ;
set T = TopStruct(# F1(),(COMPLEMENT F) #);
A4: for A, B being set st A in F & B in F holds
A \/ B in F
proof
let A, B be set ; :: thesis: ( A in F & B in F implies A \/ B in F )
assume A in F ; :: thesis: ( not B in F or A \/ B in F )
then consider A9 being Subset of F1() such that
A5: A = A9 and
A6: P1[A9] ;
assume B in F ; :: thesis: A \/ B in F
then consider B9 being Subset of F1() such that
A7: B = B9 and
A8: P1[B9] ;
 P1[A9 \/ B9] by A2, A6, A8;
hence A \/ B in F by A5, A7; :: thesis: verum
end;
A9: for G being Subset-Family of F1() st G c= F holds
Intersect G in F
proof
let G be Subset-Family of F1(); :: thesis: ( G c= F implies Intersect G in F )
assume A10: G c= F ; :: thesis: Intersect G in F
now
let A be set ; :: thesis: ( A in G implies P1[A] )
assume A in G ; :: thesis: P1[A]
then A in F by A10;
then ex B being Subset of F1() st
( A = B & P1[B] ) ;
hence P1[A] ; :: thesis: verum
end;
then P1[ Intersect G] by A3;
hence Intersect G in F ; :: thesis: verum
end;
{} c= F1() by XBOOLE_1:2;
then A11: {} in F by A1;
then reconsider T = TopStruct(# F1(),(COMPLEMENT F) #) as strict TopSpace by A9, A4, Th4;
take T ; :: thesis: ( the carrier of T = F1() & ( for A being Subset of T holds
( A is closed iff P1[A] ) ) )
thus the carrier of T = F1() ; :: thesis: for A being Subset of T holds
( A is closed iff P1[A] )
let A be Subset of T; :: thesis: ( A is closed iff P1[A] )
( A in F iff ex B being Subset of F1() st
( A = B & P1[B] ) ) ;
hence ( A is closed iff P1[A] ) by A11, A4, A9, Th4; :: thesis: verum