theorem :: CARDFIL2:79

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 is_a_convergence_point_of F2BOOL (F,T),T ) ;