let T be non empty T_1 TopSpace; :: thesis: for A being finite Subset of T holds A is closed
let A be finite Subset of T; :: thesis: A is closed
defpred S₁[ set ] means ex S being Subset of T st
( $1 = S & S is closed );
A1: S₁[ {} ]

proof

take {} T ; :: thesis: ( {} = {} T & {} T is closed )
thus {} T = {} ; :: thesis: {} T is closed
thus {} T is closed ; :: thesis: verum

end;

A2: for x, C being set st x in A & C c= A & S₁[C] holds
S₁[C \/ {x}]

proof

let x, C be set ; :: thesis: ( x in A & C c= A & S₁[C] implies S₁[C \/ {x}] )
assume that
A3: x in A and
C c= A and
A4: S₁[C] ; :: thesis: S₁[C \/ {x}]
reconsider y = x as Element of T by A3;
consider S being Subset of T such that
A5: C = S and
A6: S is closed by A4;
{y} is closed by URYSOHN1:19;
then S \/ {y} is closed by A6;
hence S₁[C \/ {x}] by A5; :: thesis: verum

end;

A7: A is finite ;
S₁[A] from FINSET_1:sch 2(A7, A1, A2);
hence A is closed ; :: thesis: verum