theorem Th9:
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) &
|[(q `1),(p `2)]| in Ball (
u,
r) &
f = <*p,|[(q `1),(p `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) )