let x be object ; :: thesis: for T being non empty TopSpace

for cF being Filter of the carrier of T st x in lim_filter cF holds

x is_a_cluster_point_of cF,T

let T be non empty TopSpace; :: thesis: for cF being Filter of the carrier of T st x in lim_filter cF holds

x is_a_cluster_point_of cF,T

let cF be Filter of the carrier of T; :: thesis: ( x in lim_filter cF implies x is_a_cluster_point_of cF,T )

assume A1: x in lim_filter cF ; :: thesis: x is_a_cluster_point_of cF,T

for cF being Filter of the carrier of T st x in lim_filter cF holds

x is_a_cluster_point_of cF,T

let T be non empty TopSpace; :: thesis: for cF being Filter of the carrier of T st x in lim_filter cF holds

x is_a_cluster_point_of cF,T

let cF be Filter of the carrier of T; :: thesis: ( x in lim_filter cF implies x is_a_cluster_point_of cF,T )

assume A1: x in lim_filter cF ; :: thesis: x is_a_cluster_point_of cF,T

now :: thesis: for A being Subset of T st A is open & x in A holds

for B being set st B in cF holds

A meets B

hence
x is_a_cluster_point_of cF,T
by WAYBEL_7:def 4; :: thesis: verumfor B being set st B in cF holds

A meets B

let A be Subset of T; :: thesis: ( A is open & x in A implies for B being set st B in cF holds

A meets B )

assume that

A2: A is open and

A3: x in A ; :: thesis: for B being set st B in cF holds

A meets B

A4: A in cF by A1, A3, A2, CARDFIL2:80, WAYBEL_7:def 5;

not {} in cF by CARD_FIL:def 1;

hence for B being set st B in cF holds

A meets B by A4, CARD_FIL:def 1; :: thesis: verum

end;A meets B )

assume that

A2: A is open and

A3: x in A ; :: thesis: for B being set st B in cF holds

A meets B

A4: A in cF by A1, A3, A2, CARDFIL2:80, WAYBEL_7:def 5;

not {} in cF by CARD_FIL:def 1;

hence for B being set st B in cF holds

A meets B by A4, CARD_FIL:def 1; :: thesis: verum