theorem Th15: :: TOPREAL4:15

for f, h being FinSequence of (TOP-REAL 2) st f /. 2 <> f /. 1 & f is being_S-Seq & (f /. 2) `1 = (f /. 1) `1 & h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|,(f /. 2)*> holds
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 & L~ h is_S-P_arc_joining f /. 1,f /. 2 & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) & L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) )