let X, x0 be set ; :: thesis: for A being Subset of (DiscrWithInfin X,x0) st A is finite holds
Cl A = A
let A be Subset of (DiscrWithInfin X,x0); :: thesis: ( A is finite implies Cl A = A )
assume A is finite ; :: thesis: Cl A = A
then A is closed by Th22;
hence Cl A = A by PRE_TOPC:52; :: thesis: verum