theorem Th37: :: TOPALG_6:37

for T being non empty TopStruct
for c being with_endpoints Curve of T
for r being Real ex c1, c2 being Element of Curves T st
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )