let X, x0 be set ; :: thesis: ( x0 in X implies for A being Subset of (DiscrWithInfin (X,x0)) st A is infinite holds
Cl A = A \/ {x0} )
assume A1: x0 in X ; :: thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A is infinite 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: ( A is infinite 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 Th20;
then A2: Cl (A9 \/ B) = A9 \/ B by PRE_TOPC:22;
assume A is infinite ; :: thesis: Cl A = A \/ {x0}
then ( not A9 is closed or x0 in A ) by A1, Th20;
hence Cl A = A \/ {x0} by A2, Th25, ZFMISC_1:40; :: thesis: verum