theorem Th17:
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 &
q1 <> q2 holds
ex
g being
Function of
I[01],
((TOP-REAL 2) | A) ex
s1,
s2 being
Real st
(
g is
being_homeomorphism &
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 &
g . s2 = q2 &
0 <= s1 &
s1 < s2 &
s2 <= 1 )