let T be non empty TopSpace; :: thesis: for F being proper Filter of (BoolePoset ([#] T))
for x being Point of T holds
( x in Lim (a_net F) iff x is_a_convergence_point_of F,T )
let F be proper Filter of (BoolePoset ([#] T)); :: thesis: for x being Point of T holds
( x in Lim (a_net F) iff x is_a_convergence_point_of F,T )
F = a_filter (a_net F) by Th14;
hence for x being Point of T holds
( x in Lim (a_net F) iff x is_a_convergence_point_of F,T ) by Th12; :: thesis: verum