for T being non empty TopSpace
for x being Point of T
for F being Filter of the carrier of T holds
( x is_a_convergence_point_of F,T iff x in lim_filter F )