theorem Th6: :: TOPALG_6:6

for T being non empty TopSpace
for S being non empty SubSpace of T
for t1, t2 being Point of T
for s1, s2 being Point of S
for A, B being Path of t1,t2
for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds
A,B are_homotopic