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 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 ; :: 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 )

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 ; :: 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 A6; :: thesis: verum

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 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 ; :: 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 )

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 ; :: 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 A6; :: thesis: verum