:: deftheorem defines is_isolated_in TOPGEN_1:def 4 :
for T being TopSpace
for A being Subset of T
for x being set holds
( x is_isolated_in A iff ( x in A & not x is_an_accumulation_point_of A ) );