theorem Th9: :: RCOMP_1:9

for s1 being Real_Sequence
for X being Subset of REAL st ( for p being Real st p in X holds
ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((s1 . m) - p).| ) ) ) holds
for s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent holds
not lim s2 in X