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
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
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;
hence x is_a_cluster_point_of cF,T by WAYBEL_7:def 4; :: thesis: verum