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