:: deftheorem defines is_an_accumulation_point_of TOPGEN_1:def 2 :
for T being TopStruct
for A being Subset of T
for x being object holds
( x is_an_accumulation_point_of A iff x in Cl (A \ {x}) );