let T be TopSpace; :: thesis: for A being Subset of T
for x being set st x is_an_accumulation_point_of A holds
x is Point of T
let A be Subset of T; :: thesis: for x being set st x is_an_accumulation_point_of A holds
x is Point of T
let x be set ; :: thesis: ( x is_an_accumulation_point_of A implies x is Point of T )
assume x is_an_accumulation_point_of A ; :: thesis: x is Point of T
then x in Cl (A \ {x}) by Def2;
hence x is Point of T ; :: thesis: verum