:: deftheorem defines isolated TOPGEN_1:def 5 :
for T being TopSpace
for p being Point of T holds
( p is isolated iff p is_isolated_in [#] T );