let p, q be Point of (TOP-REAL 2); :: thesis: 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 ),(((p `2 ) + (q `2 )) / 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); :: thesis: 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 ),(((p `2 ) + (q `2 )) / 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; :: thesis: 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 ),(((p `2 ) + (q `2 )) / 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); :: thesis: ( p `1 = q `1 & p `2 <> q `2 & p in Ball u,r & q in Ball u,r & f = <*p,|[(p `1 ),(((p `2 ) + (q `2 )) / 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 A1: ( p `1 = q `1 & p `2 <> q `2 & p in Ball u,r & q in Ball u,r & f = <*p,|[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|,q*> ) ; :: thesis: ( 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 )
hence ( f is being_S-Seq & f /. 1 = p & f /. (len f) = q ) by TOPREAL3:43; :: thesis: ( L~ f is_S-P_arc_joining p,q & L~ f c= Ball u,r )
hence L~ f is_S-P_arc_joining p,q by Def1; :: thesis: L~ f c= Ball u,r
( p = |[(p `1 ),(p `2 )]| & q = |[(q `1 ),(q `2 )]| ) by EUCLID:57;
then A2: ( L~ f = (LSeg p,|[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|) \/ (LSeg |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|,q) & |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| in Ball u,r ) by A1, TOPREAL3:23, TOPREAL3:30;
then ( LSeg p,|[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| c= Ball u,r & LSeg |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|,q c= Ball u,r ) by A1, TOPREAL3:28;
hence L~ f c= Ball u,r by A2, XBOOLE_1:8; :: thesis: verum