theorem Th20:
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
p,
q being
Path of
t1,
t2 st
p = pr2 l1 &
q = pr2 l2 &
l1,
l2 are_homotopic holds
p,
q are_homotopic