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 Th20;
hence Cl A = A by PRE_TOPC:22; :: thesis: verum