for p, q being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2)
for r being Real
for u being Point of (Euclid 2) st p `1 <> q `1 & p `2 <> q `2 & p in Ball (u,r) & q in Ball (u,r) & |[(p `1),(q `2)]| in Ball (u,r) & f = <*p,|[(p `1),(q `2)]|,q*> holds
( f is being_S-Seq & f /. 1 = p & f /. (len f) = q & L~ f is_S-P_arc_joining p,q & L~ f c= Ball (u,r) )