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:34; ( 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:21;
thus
L~ f is_S-P_arc_joining p,q
by A6; 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:16, TOPREAL3:21;
hence
L~ f c= Ball (u,r)
by A7, XBOOLE_1:8; verum