:: deftheorem defines is_a_cluster_point_of FRECHET2:def 3 :
for T being TopStruct
for S being sequence of T
for x being Point of T holds
( x is_a_cluster_point_of S iff for O being Subset of T
for n being Nat st O is open & x in O holds
ex m being Element of NAT st
( n <= m & S . m in O ) );