let X, x0 be set ; :: thesis: ( x0 in X implies for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds
Int A = A \ {x0} )
assume A1: x0 in X ; :: thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds
Int 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 Int A = A \ {x0} )
reconsider A9 = A as Subset of T ;
assume A ` is infinite ; :: thesis: Int A = A \ {x0}
then Cl (A `) = (A9 `) \/ {x} by A1, Th26;
hence Int A = ((A9 `) \/ {x}) ` by TOPS_1:def 1
.= ((A9 \ {x}) `) ` by SUBSET_1:14
.= A \ {x0} ;
:: thesis: verum