defpred S_{1}[ set ] means ( ( $1 c= X & $1 is finite ) or $1 = X );

A1: X c= X ;

A2: for A, B being set st S_{1}[A] & S_{1}[B] holds

S_{1}[A \/ B]

S_{1}[A] ) holds

S_{1}[ Intersect G]
_{1}[ {} ] & S_{1}[X] )
by XBOOLE_1:2;

consider T being strict TopSpace such that

A13: ( the carrier of T = X & ( for A being Subset of T holds

( A is closed iff S_{1}[A] ) ) )
from TOPGEN_3:sch 1(A12, A2, A5);

take T ; :: thesis: ( the carrier of T = X & ( for F being Subset of T holds

( F is closed iff ( F is finite or F = X ) ) ) )

thus the carrier of T = X by A13; :: thesis: for F being Subset of T holds

( F is closed iff ( F is finite or F = X ) )

let F be Subset of T; :: thesis: ( F is closed iff ( F is finite or F = X ) )

thus ( F is closed iff ( F is finite or F = X ) ) by A13; :: thesis: verum

A1: X c= X ;

A2: for A, B being set st S

S

proof

A5:
for G being Subset-Family of X st ( for A being set st A in G holds
let A, B be set ; :: thesis: ( S_{1}[A] & S_{1}[B] implies S_{1}[A \/ B] )

assume that

A3: S_{1}[A]
and

A4: S_{1}[B]
; :: thesis: S_{1}[A \/ B]

reconsider A = A, B = B as Subset of X by A3, A4, A1;

A \/ B c= X ;

hence S_{1}[A \/ B]
by A3, A4, XBOOLE_1:12; :: thesis: verum

end;assume that

A3: S

A4: S

reconsider A = A, B = B as Subset of X by A3, A4, A1;

A \/ B c= X ;

hence S

S

S

proof

A12:
( S
let G be Subset-Family of X; :: thesis: ( ( for A being set st A in G holds

S_{1}[A] ) implies S_{1}[ Intersect G] )

assume A6: for A being set st A in G holds

S_{1}[A]
; :: thesis: S_{1}[ Intersect G]

_{1}[ Intersect G]
by A1, MSSUBFAM:9, SETFAM_1:def 9; :: thesis: verum

end;S

assume A6: for A being set st A in G holds

S

now :: thesis: ( G <> {} & G <> {X} implies ( Intersect G is finite & Intersect G c= X ) )

hence
Sassume that

A7: G <> {} and

A8: G <> {X} ; :: thesis: ( Intersect G is finite & Intersect G c= X )

not G c= {X} by A7, A8, ZFMISC_1:33;

then consider a being object such that

A9: a in G and

A10: not a in {X} ;

reconsider aa = a as set by TARSKI:1;

A11: a <> X by A10, TARSKI:def 1;

S_{1}[aa]
by A6, A9;

hence ( Intersect G is finite & Intersect G c= X ) by A11, A9, FINSET_1:1, MSSUBFAM:2; :: thesis: verum

end;A7: G <> {} and

A8: G <> {X} ; :: thesis: ( Intersect G is finite & Intersect G c= X )

not G c= {X} by A7, A8, ZFMISC_1:33;

then consider a being object such that

A9: a in G and

A10: not a in {X} ;

reconsider aa = a as set by TARSKI:1;

A11: a <> X by A10, TARSKI:def 1;

S

hence ( Intersect G is finite & Intersect G c= X ) by A11, A9, FINSET_1:1, MSSUBFAM:2; :: thesis: verum

consider T being strict TopSpace such that

A13: ( the carrier of T = X & ( for A being Subset of T holds

( A is closed iff S

take T ; :: thesis: ( the carrier of T = X & ( for F being Subset of T holds

( F is closed iff ( F is finite or F = X ) ) ) )

thus the carrier of T = X by A13; :: thesis: for F being Subset of T holds

( F is closed iff ( F is finite or F = X ) )

let F be Subset of T; :: thesis: ( F is closed iff ( F is finite or F = X ) )

thus ( F is closed iff ( F is finite or F = X ) ) by A13; :: thesis: verum