let T be non empty TopStruct ; :: thesis: for S being sequence of T
for x being Point of T st S is_convergent_to x holds
x is_a_cluster_point_of S
let S be sequence of T; :: thesis: for x being Point of T st S is_convergent_to x holds
x is_a_cluster_point_of S
let x be Point of T; :: thesis: ( S is_convergent_to x implies x is_a_cluster_point_of S )
assume A1: S is_convergent_to x ; :: thesis: x is_a_cluster_point_of S
ex S1 being subsequence of S st S1 is_convergent_to x
proof
reconsider S1 = S as subsequence of S by VALUED_0:19;
take S1 ; :: thesis: S1 is_convergent_to x
thus S1 is_convergent_to x by A1; :: thesis: verum
end;
hence x is_a_cluster_point_of S by Th31; :: thesis: verum