let P be 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) | P)
for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & 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
let p1, p2, q1, q2 be Point of (TOP-REAL 2); for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & 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
let g be Function of I[01],((TOP-REAL 2) | P); for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & 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
let s1, s2 be Real; ( P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 implies LE q1,q2,P,p1,p2 )
assume that
A1:
P is_an_arc_of p1,p2
and
A2:
g is being_homeomorphism
and
A3:
g . 0 = p1
and
A4:
g . 1 = p2
and
A5:
g . s1 = q1
and
A6:
( 0 <= s1 & s1 <= 1 )
and
A7:
g . s2 = q2
and
A8:
( 0 <= s2 & s2 <= 1 )
and
A9:
s1 <= s2
; LE q1,q2,P,p1,p2
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
s1 in the carrier of I[01]
by A6, BORSUK_1:43;
then A10:
q1 in [#] ((TOP-REAL 2) | P9)
by A5, FUNCT_2:5;
reconsider g = g as Function of I[01],((TOP-REAL 2) | P9) ;
s2 in the carrier of I[01]
by A8, BORSUK_1:43;
then
g . s2 in the carrier of ((TOP-REAL 2) | P9)
by FUNCT_2:5;
then A11:
q2 in P
by A7, A10, PRE_TOPC:def 5;
A12:
now for h being Function of I[01],((TOP-REAL 2) | P9)
for t1, t2 being Real st h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 holds
t1 <= t2reconsider s19 =
s1,
s29 =
s2 as
Point of
I[01] by A6, A8, BORSUK_1:43;
let h be
Function of
I[01],
((TOP-REAL 2) | P9);
for t1, t2 being Real st h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 holds
b4 <= b5let t1,
t2 be
Real;
( h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 implies b2 <= b3 )assume that A13:
h is
being_homeomorphism
and A14:
h . 0 = p1
and A15:
h . 1
= p2
and A16:
h . t1 = q1
and A17:
(
0 <= t1 &
t1 <= 1 )
and A18:
h . t2 = q2
and A19:
(
0 <= t2 &
t2 <= 1 )
;
b2 <= b3A20:
h is
one-to-one
by A13, TOPS_2:def 5;
set hg =
(h ") * g;
h " is
being_homeomorphism
by A13, TOPS_2:56;
then
(h ") * g is
being_homeomorphism
by A2, TOPS_2:57;
then A21:
(
(h ") * g is
continuous &
(h ") * g is
one-to-one )
by TOPS_2:def 5;
reconsider hg1 =
((h ") * g) . s19,
hg2 =
((h ") * g) . s29 as
Real by BORSUK_1:40;
A22:
dom g = [#] I[01]
by A2, TOPS_2:def 5;
then A23:
0 in dom g
by BORSUK_1:43;
A24:
dom h = [#] I[01]
by A13, TOPS_2:def 5;
then A25:
t1 in dom h
by A17, BORSUK_1:43;
A26:
0 in dom h
by A24, BORSUK_1:43;
rng h = [#] ((TOP-REAL 2) | P)
by A13, TOPS_2:def 5;
then
h is
onto
by FUNCT_2:def 3;
then A27:
h " = h "
by A20, TOPS_2:def 4;
then
(h ") . p1 = 0
by A14, A26, A20, FUNCT_1:32;
then A28:
((h ") * g) . 0 = 0
by A3, A23, FUNCT_1:13;
s1 in dom g
by A6, A22, BORSUK_1:43;
then A29:
((h ") * g) . s1 =
(h ") . q1
by A5, FUNCT_1:13
.=
t1
by A16, A20, A25, A27, FUNCT_1:32
;
A30:
t2 in dom h
by A19, A24, BORSUK_1:43;
s2 in dom g
by A8, A22, BORSUK_1:43;
then A31:
((h ") * g) . s2 =
(h ") . q2
by A7, FUNCT_1:13
.=
t2
by A18, A20, A30, A27, FUNCT_1:32
;
A32:
1
in dom g
by A22, BORSUK_1:43;
A33:
1
in dom h
by A24, BORSUK_1:43;
(h ") . p2 = 1
by A15, A33, A20, A27, FUNCT_1:32;
then A34:
((h ") * g) . 1
= 1
by A4, A32, FUNCT_1:13;
end;
q1 in P
by A10, PRE_TOPC:def 5;
hence
LE q1,q2,P,p1,p2
by A11, A12; verum