set X = F₁();
set F = { A where A is Subset of F₁() : P₁[A] } ;
{ A where A is Subset of F₁() : P₁[A] } c= bool F₁()

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { A where A is Subset of F₁() : P₁[A] } or a in bool F₁() )
assume a in { A where A is Subset of F₁() : P₁[A] } ; :: thesis: a in bool F₁()
then ex B being Subset of F₁() st
( a = B & P₁[B] ) ;
hence a in bool F₁() ; :: thesis: verum

end;

then reconsider F = { A where A is Subset of F₁() : P₁[A] } as Subset-Family of F₁() ;
set T = TopStruct(# F₁(),(COMPLEMENT F) #);
( {} c= F₁() & F₁() c= F₁() ) by XBOOLE_1:2;
then A4: ( {} in F & F₁() in F ) by A1;
A5: 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 A' being Subset of F₁() such that
A6: ( A = A' & P₁[A'] ) ;
assume B in F ; :: thesis: A \/ B in F
then consider B' being Subset of F₁() such that
A7: ( B = B' & P₁[B'] ) ;
P₁[A' \/ B'] by A2, A6, A7;
hence A \/ B in F by A6, A7; :: thesis: verum

end;

A8: for G being Subset-Family of F₁() st G c= F holds
Intersect G in F

proof

let G be Subset-Family of F₁(); :: thesis: ( G c= F implies Intersect G in F )
assume A9: G c= F ; :: thesis: Intersect G in F

now

let A be set ; :: thesis: ( A in G implies P₁[A] )
assume A in G ; :: thesis: P₁[A]
then A in F by A9;
then ex B being Subset of F₁() st
( A = B & P₁[B] ) ;
hence P₁[A] ; :: thesis: verum

end;

then P₁[ Intersect G] by A3;
hence Intersect G in F ; :: thesis: verum

end;

then reconsider T = TopStruct(# F₁(),(COMPLEMENT F) #) as strict TopSpace by A4, A5, Th4;
take T ; :: thesis: ( the carrier of T = F₁() & ( for A being Subset of T holds
( A is closed iff P₁[A] ) ) )
thus the carrier of T = F₁() ; :: thesis: for A being Subset of T holds
( A is closed iff P₁[A] )
let A be Subset of T; :: thesis: ( A is closed iff P₁[A] )
( ( A in F implies ex B being Subset of F₁() st
( A = B & P₁[B] ) ) & ( ex B being Subset of F₁() st
( A = B & P₁[B] ) implies A in F ) & ( A is closed implies A in F ) & ( A in F implies A is closed ) ) by A4, A5, A8, Th4;
hence ( A is closed iff P₁[A] ) ; :: thesis: verum