let T be non empty TopSpace; :: thesis: for N being net of T
for x being Point of T holds
( x in Lim N iff x is_a_convergence_point_of a_filter N,T )
let N be net of T; :: thesis: for x being Point of T holds
( x in Lim N iff x is_a_convergence_point_of a_filter N,T )
set F = a_filter N;
let x be Point of T; :: thesis: ( x in Lim N iff x is_a_convergence_point_of a_filter N,T )
thus ( x in Lim N implies x is_a_convergence_point_of a_filter N,T ) :: thesis: ( x is_a_convergence_point_of a_filter N,T implies x in Lim N )
proof
assume A1: x in Lim N ; :: thesis: x is_a_convergence_point_of a_filter N,T
let A be Subset of T; :: according to WAYBEL_7:def 5 :: thesis: ( not A is open or not x in A or A in a_filter N )
assume that
A2: A is open and
A3: x in A ; :: thesis: A in a_filter N
A is a_neighborhood of x by A2, A3, CONNSP_2:3;
then N is_eventually_in A by A1, YELLOW_6:def 15;
hence A in a_filter N ; :: thesis: verum
end;
assume A4: for A being Subset of T st A is open & x in A holds
A in a_filter N ; :: according to WAYBEL_7:def 5 :: thesis: x in Lim N
now :: thesis: for O being a_neighborhood of x holds N is_eventually_in O
let O be a_neighborhood of x; :: thesis: N is_eventually_in O
x in Int O by CONNSP_2:def 1;
then Int O in a_filter N by A4;
then A5: N is_eventually_in Int O by Th10;
Int O c= O by TOPS_1:16;
hence N is_eventually_in O by A5, WAYBEL_0:8; :: thesis: verum
end;
hence x in Lim N by YELLOW_6:def 15; :: thesis: verum