theorem Th11: :: TOPREAL4:11

for p being Point of (TOP-REAL 2)
for f, h being FinSequence of (TOP-REAL 2) st p <> f /. 1 & (f /. 1) `2 = p `2 & f is being_S-Seq & p in LSeg (f,1) & h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*> holds
( 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 | 1)) \/ (LSeg ((f /. 1),p)) )