theorem Th18:
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) for
g being
Function of
I[01],
(TOP-REAL 2) for
s1,
s2 being
Real st
P is_an_arc_of p1,
p2 &
g is
continuous &
g is
one-to-one &
rng g = P &
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 &
0 <= s1 &
s1 <= 1 &
g . s2 = q2 &
0 <= s2 &
s2 <= 1 &
s1 <= s2 holds
LE q1,
q2,
P,
p1,
p2