:: deftheorem defines is_a_cluster_point_of WAYBEL_7:def 4 :
for T being TopSpace
for F being set
for x being object holds
( x is_a_cluster_point_of F,T iff for A being Subset of T st A is open & x in A holds
for B being set st B in F holds
A meets B );