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 A' = A as Subset of T ;
x0 in {x0} by TARSKI:def 1;
then x0 in A' \/ B by XBOOLE_0:def 3;
then A' \/ B is closed by Th22;
then A2: Cl (A' \/ B) = A' \/ B by PRE_TOPC:52;
assume not A is finite ; :: thesis: Cl A = A \/ {x0}
then ( not A' is closed or x0 in A ) by A1, Th22;
hence Cl A = A \/ {x0} by A2, Th27, ZFMISC_1:46; :: thesis: verum