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

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