defpred S₁[ set ] means ( ( $1 c= X & $1 is finite ) or $1 = X );
A1: X c= X ;
A2: for A, B being set st S₁[A] & S₁[B] holds
S₁[A \/ B]

proof

let A, B be set ; :: thesis: ( S₁[A] & S₁[B] implies S₁[A \/ B] )
assume that
A3: S₁[A] and
A4: S₁[B] ; :: thesis: S₁[A \/ B]
reconsider A = A, B = B as Subset of X by A3, A4, A1;
A \/ B c= X ;
hence S₁[A \/ B] by A3, A4, XBOOLE_1:12; :: thesis: verum

end;

A5: for G being Subset-Family of X st ( for A being set st A in G holds
S₁[A] ) holds
S₁[ Intersect G]

proof

let G be Subset-Family of X; :: thesis: ( ( for A being set st A in G holds
S₁[A] ) implies S₁[ Intersect G] )
assume A6: for A being set st A in G holds
S₁[A] ; :: thesis: S₁[ Intersect G]

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

assume 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₁[aa] by A6, A9;
hence ( Intersect G is finite & Intersect G c= X ) by A11, A9, FINSET_1:1, MSSUBFAM:2; :: thesis: verum

end;

hence S₁[ Intersect G] by A1, MSSUBFAM:9, SETFAM_1:def 9; :: thesis: verum

end;

A12: ( S₁[ {} ] & S₁[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₁[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