theorem :: TOPREAL3:26

for f being FinSequence of (TOP-REAL 2)
for r being Real
for u being Point of (Euclid 2)
for m being Nat st not f /. 1 in Ball (u,r) & 1 <= m & m <= (len f) - 1 & ( for i being Nat st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds
m <= i ) holds
not f /. m in Ball (u,r)