:: deftheorem defines is_a_cluster_point_of WAYBEL_9:def 9 :
for T being non empty TopSpace
for N being non empty NetStr over T
for p being Point of T holds
( p is_a_cluster_point_of N iff for O being a_neighborhood of p holds N is_often_in O );