theorem
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T for
l1,
l2 being
Path of
[s1,t1],
[s2,t2] for
H being
Homotopy of
l1,
l2 for
p,
q being
Path of
t1,
t2 st
p = pr2 l1 &
q = pr2 l2 &
l1,
l2 are_homotopic holds
pr2 H is
Homotopy of
p,
q