set X = F_{1}();

set F = { A where A is Subset of F_{1}() : P_{1}[A] } ;

{ A where A is Subset of F_{1}() : P_{1}[A] } c= bool F_{1}()
_{1}() : P_{1}[A] } as Subset-Family of F_{1}() ;

set T = TopStruct(# F_{1}(),(COMPLEMENT F) #);

A4: for A, B being set st A in F & B in F holds

A \/ B in F_{1}() st G c= F holds

Intersect G in F_{1}()
;

then A11: {} in F by A1;

then reconsider T = TopStruct(# F_{1}(),(COMPLEMENT F) #) as strict TopSpace by A9, A4, Th4;

take T ; :: thesis: ( the carrier of T = F_{1}() & ( for A being Subset of T holds

( A is closed iff P_{1}[A] ) ) )

thus the carrier of T = F_{1}()
; :: thesis: for A being Subset of T holds

( A is closed iff P_{1}[A] )

let A be Subset of T; :: thesis: ( A is closed iff P_{1}[A] )

( A in F iff ex B being Subset of F_{1}() st

( A = B & P_{1}[B] ) )
;

hence ( A is closed iff P_{1}[A] )
by A11, A4, A9, Th4; :: thesis: verum

set F = { A where A is Subset of F

{ A where A is Subset of F

proof

then reconsider F = { A where A is Subset of F
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { A where A is Subset of F_{1}() : P_{1}[A] } or a in bool F_{1}() )

assume a in { A where A is Subset of F_{1}() : P_{1}[A] }
; :: thesis: a in bool F_{1}()

then ex B being Subset of F_{1}() st

( a = B & P_{1}[B] )
;

hence a in bool F_{1}()
; :: thesis: verum

end;assume a in { A where A is Subset of F

then ex B being Subset of F

( a = B & P

hence a in bool F

set T = TopStruct(# F

A4: for A, B being set st A in F & B in F holds

A \/ B in F

proof

A9:
for G being Subset-Family of F
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 F_{1}() such that

A5: A = A9 and

A6: P_{1}[A9]
;

assume B in F ; :: thesis: A \/ B in F

then consider B9 being Subset of F_{1}() such that

A7: B = B9 and

A8: P_{1}[B9]
;

P_{1}[A9 \/ B9]
by A2, A6, A8;

hence A \/ B in F by A5, A7; :: thesis: verum

end;assume A in F ; :: thesis: ( not B in F or A \/ B in F )

then consider A9 being Subset of F

A5: A = A9 and

A6: P

assume B in F ; :: thesis: A \/ B in F

then consider B9 being Subset of F

A7: B = B9 and

A8: P

P

hence A \/ B in F by A5, A7; :: thesis: verum

Intersect G in F

proof

{} c= F
let G be Subset-Family of F_{1}(); :: thesis: ( G c= F implies Intersect G in F )

assume A10: G c= F ; :: thesis: Intersect G in F

_{1}[ Intersect G]
by A3;

hence Intersect G in F ; :: thesis: verum

end;assume A10: G c= F ; :: thesis: Intersect G in F

now :: thesis: for A being set st A in G holds

P_{1}[A]

then
PP

let A be set ; :: thesis: ( A in G implies P_{1}[A] )

assume A in G ; :: thesis: P_{1}[A]

then A in F by A10;

then ex B being Subset of F_{1}() st

( A = B & P_{1}[B] )
;

hence P_{1}[A]
; :: thesis: verum

end;assume A in G ; :: thesis: P

then A in F by A10;

then ex B being Subset of F

( A = B & P

hence P

hence Intersect G in F ; :: thesis: verum

then A11: {} in F by A1;

then reconsider T = TopStruct(# F

take T ; :: thesis: ( the carrier of T = F

( A is closed iff P

thus the carrier of T = F

( A is closed iff P

let A be Subset of T; :: thesis: ( A is closed iff P

( A in F iff ex B being Subset of F

( A = B & P

hence ( A is closed iff P