theorem Th17: :: TOPREAL4:17

for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2)
for n being Nat st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) 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 & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )