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