let X, x0 be set ; :: thesis: ( x0 in X implies for A being Subset of (DiscrWithInfin (X,x0)) st not A is finite holds
Cl A = A \/ {x0} )
assume A1: x0 in X ; :: thesis: for A being Subset of (DiscrWithInfin (X,x0)) st not A is finite holds
Cl A = A \/ {x0}
set T = DiscrWithInfin (X,x0);
reconsider T = DiscrWithInfin (X,x0) as non empty TopSpace by A1;
reconsider x = x0 as Point of T by A1, Def5;
let A be Subset of (DiscrWithInfin (X,x0)); :: thesis: ( not A is finite implies Cl A = A \/ {x0} )
reconsider B = {x} as Subset of T ;
reconsider A9 = A as Subset of T ;
x0 in {x0} by TARSKI:def 1;
then x0 in A9 \/ B by XBOOLE_0:def 3;
then A9 \/ B is closed by Th22;
then A2: Cl (A9 \/ B) = A9 \/ B by PRE_TOPC:22;
assume not A is finite ; :: thesis: Cl A = A \/ {x0}
then ( not A9 is closed or x0 in A ) by A1, Th22;
hence Cl A = A \/ {x0} by A2, Th27, ZFMISC_1:40; :: thesis: verum