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 )

A in a_filter N ; :: according to WAYBEL_7:def 5 :: thesis: x in Lim N

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 A4:
for A being Subset of T st A is open & x in A holds
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;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

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

hence
x in Lim N
by YELLOW_6:def 15; :: thesis: verumlet 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;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