let p be Point of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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 Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
set p1 = f /. 1;
assume A1: ( p <> f /. 1 & f is being_S-Seq & p in L~ f ) ; :: thesis: 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 )
then consider X being set such that
A2: ( p in X & X in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ) by TARSKI:def 4;
consider n being Element of NAT such that
A3: ( X = LSeg f,n & 1 <= n & n + 1 <= len f ) by A2;
consider h being FinSequence of (TOP-REAL 2) such that
A4: ( 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 & L~ h = (L~ (f | n)) \/ (LSeg (f /. n),p) ) by A1, A2, A3, Th18;
take h ; :: thesis: ( 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 A4; :: thesis: verum