let p be Point of (TOP-REAL 2); for f being FinSequence of (TOP-REAL 2) st p <> f /. 1 & f is being_S-Seq & p in L~ f holds
ex h being FinSequence of (TOP-REAL 2) st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f )
let f be FinSequence of (TOP-REAL 2); ( p <> f /. 1 & f is being_S-Seq & p in L~ f implies ex h being FinSequence of (TOP-REAL 2) st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f ) )
set M = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
set p1 = f /. 1;
assume that
A1:
( p <> f /. 1 & f is being_S-Seq )
and
A2:
p in L~ f
; ex h being FinSequence of (TOP-REAL 2) st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f )
consider X being set such that
A3:
p in X
and
A4:
X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by A2, TARSKI:def 4;
consider n being Nat such that
A5:
X = LSeg (f,n)
and
1 <= n
and
n + 1 <= len f
by A4;
consider h being FinSequence of (TOP-REAL 2) such that
A6:
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f )
and
L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p))
by A1, A3, A5, Th17;
take
h
; ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f )
thus
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f )
by A6; verum