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

take {} T ; :: thesis:
thus {} T = {} ; :: thesis:
thus {} T is closed ; :: thesis:

end;

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

let x, C be set ; :: thesis:
assume that
A3: x in A and
C c= A and
A4: S₁[C] ; :: thesis:
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:

end;