:: deftheorem Def9 defines without_isolated_points PENCIL_1:def 9 :
for S being TopStruct holds
( S is without_isolated_points iff for x being Point of S ex l being Block of S st x in l );