:: deftheorem Def5 defines contains_almost_all_sequence METRIC_6:def 5 :
for X being non empty MetrSpace
for V being Subset of X
for S being sequence of X holds
( V contains_almost_all_sequence S iff ex m being Nat st
for n being Nat st m <= n holds
S . n in V );