let T be non empty TopSpace; :: thesis: for N being net of T
for x being Point of T holds
( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T )
let N be net of T; :: thesis: for x being Point of T holds
( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T )
set F = a_filter N;
let x be Point of T; :: thesis: ( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T )
thus ( x is_a_cluster_point_of N implies x is_a_cluster_point_of a_filter N,T ) :: thesis: ( x is_a_cluster_point_of a_filter N,T implies x is_a_cluster_point_of N )

proof

assume A1: for O being a_neighborhood of x holds N is_often_in O ; :: according to WAYBEL_9:def 9 :: thesis: x is_a_cluster_point_of a_filter N,T
let A be Subset of T; :: according to WAYBEL_7:def 4 :: thesis: ( not A is open or not x in A or for b₁ being set holds
( not b₁ in a_filter N or not A misses b₁ ) )
assume that
A2: A is open and
A3: x in A ; :: thesis: for b₁ being set holds
( not b₁ in a_filter N or not A misses b₁ )
let B be set ; :: thesis: ( not B in a_filter N or not A misses B )
assume B in a_filter N ; :: thesis: not A misses B
then N is_eventually_in B by Th10;
then consider i being Element of N such that
A4: for j being Element of N st i <= j holds
N . j in B ;
A is a_neighborhood of x by A2, A3, CONNSP_2:3;
then N is_often_in A by A1;
then ex j being Element of N st
( i <= j & N . j in A ) ;
then ex a being Point of T st
( a in B & a in A ) by A4;
hence not A misses B by XBOOLE_0:3; :: thesis: verum

end;

assume A5: for A being Subset of T st A is open & x in A holds
for B being set st B in a_filter N holds
A meets B ; :: according to WAYBEL_7:def 4 :: thesis: x is_a_cluster_point_of N
let O be a_neighborhood of x; :: according to WAYBEL_9:def 9 :: thesis: N is_often_in O
let i be Element of N; :: according to WAYBEL_0:def 12 :: thesis: ex b₁ being Element of the carrier of N st
( i <= b₁ & N . b₁ in O )
reconsider B = rng the mapping of (N | i) as Subset of T,N by Def2;
N is_eventually_in B by Th8;
then A6: B in a_filter N ;
x in Int O by CONNSP_2:def 1;
then Int O meets B by A5, A6;
then consider x being object such that
A7: x in Int O and
A8: x in B by XBOOLE_0:3;
consider j being Element of N such that
A9: i <= j and
A10: x = N . j by A8, Th7;
take j ; :: thesis: ( i <= j & N . j in O )
Int O c= O by TOPS_1:16;
hence ( i <= j & N . j in O ) by A7, A9, A10; :: thesis: verum