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 )

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_{1} being Element of the carrier of N st

( i <= b_{1} & N . b_{1} 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

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 A5:
for A being Subset of T st A is open & x in A holds
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_{1} being set holds

( not b_{1} in a_filter N or not A misses b_{1} ) )

assume that

A2: A is open and

A3: x in A ; :: thesis: for b_{1} being set holds

( not b_{1} in a_filter N or not A misses b_{1} )

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;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

( not b

assume that

A2: A is open and

A3: x in A ; :: thesis: for b

( not 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

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

( i <= b

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