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 & |[(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 )
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 & |[(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 )
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 & |[(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 )
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 & |[(p `1 ),(q `2 )]| in Ball u,r & f = <*p,|[(p `1 ),(q `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 & p `2 <> q `2 )
and
A2:
p in Ball u,r
and
A3:
q in Ball u,r
and
A4:
|[(p `1 ),(q `2 )]| in Ball u,r
and
A5:
f = <*p,|[(p `1 ),(q `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 A6:
( f is being_S-Seq & f /. 1 = p & f /. (len f) = q )
by A1, A5, TOPREAL3:41; ( L~ f is_S-P_arc_joining p,q & L~ f c= Ball u,r )
A7:
LSeg |[(p `1 ),(q `2 )]|,q c= Ball u,r
by A3, A4, TOPREAL3:28;
thus
L~ f is_S-P_arc_joining p,q
by A6, Def1; L~ f c= Ball u,r
( L~ f = (LSeg p,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,q) & LSeg p,|[(p `1 ),(q `2 )]| c= Ball u,r )
by A2, A4, A5, TOPREAL3:23, TOPREAL3:28;
hence
L~ f c= Ball u,r
by A7, XBOOLE_1:8; verum