let p, q be 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) & f = <*p,|[(((p `1) + (q `1)) / 2),(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) )
let f be 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) & f = <*p,|[(((p `1) + (q `1)) / 2),(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) )
let r be 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) & f = <*p,|[(((p `1) + (q `1)) / 2),(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) )
let u be Point of (Euclid 2); ( p `1 <> q `1 & p `2 = q `2 & p in Ball (u,r) & q in Ball (u,r) & f = <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> implies ( 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) ) )
assume that
A1:
p `1 <> q `1
and
A2:
p `2 = q `2
and
A3:
( p in Ball (u,r) & q in Ball (u,r) )
and
A4:
f = <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*>
; ( 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) )
thus A5:
( f is being_S-Seq & f /. 1 = p & f /. (len f) = q )
by A1, A2, A4, TOPREAL3:37; ( L~ f is_S-P_arc_joining p,q & L~ f c= Ball (u,r) )
( p = |[(p `1),(p `2)]| & q = |[(q `1),(q `2)]| )
by EUCLID:53;
then
|[(((p `1) + (q `1)) / 2),(p `2)]| in Ball (u,r)
by A2, A3, TOPREAL3:24;
then A6:
( LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|) c= Ball (u,r) & LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q) c= Ball (u,r) )
by A3, TOPREAL3:21;
thus
L~ f is_S-P_arc_joining p,q
by A5; L~ f c= Ball (u,r)
L~ f = (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) \/ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q))
by A4, TOPREAL3:16;
hence
L~ f c= Ball (u,r)
by A6, XBOOLE_1:8; verum