theorem Th16:
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T st
s1,
s2 are_connected &
t1,
t2 are_connected holds
for
L1 being
Path of
s1,
s2 for
L2 being
Path of
t1,
t2 holds
<:L1,L2:> is
Path of
[s1,t1],
[s2,t2]