theorem Th14: :: TOPREAL4:14

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