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:4;
A10:
s1 in the carrier of I[01]
by A6, BORSUK_1:86;
then A11:
q1 in [#] ((TOP-REAL 2) | P9)
by A5, FUNCT_2:7;
reconsider g = g as Function of I[01] ,((TOP-REAL 2) | P9) ;
A12:
s2 in the carrier of I[01]
by A8, BORSUK_1:86;
then
g . s2 in the carrier of ((TOP-REAL 2) | P9)
by FUNCT_2:7;
then A13:
q2 in P
by A7, A11, PRE_TOPC:def 10;
A14:
now reconsider s19 =
s1,
s29 =
s2 as
Point of
I[01] by A6, A8, BORSUK_1:86;
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 A15:
h is
being_homeomorphism
and A16:
h . 0 = p1
and A17:
h . 1
= p2
and A18:
h . t1 = q1
and A19:
(
0 <= t1 &
t1 <= 1 )
and A20:
h . t2 = q2
and A21:
(
0 <= t2 &
t2 <= 1 )
;
b2 <= b3A22:
h is
one-to-one
by A15, TOPS_2:def 5;
set hg =
(h " ) * g;
h " is
being_homeomorphism
by A15, TOPS_2:70;
then
(h " ) * g is
being_homeomorphism
by A2, TOPS_2:71;
then A23:
(
(h " ) * g is
continuous &
(h " ) * g is
one-to-one )
by TOPS_2:def 5;
(
((h " ) * g) . s1 in the
carrier of
I[01] &
((h " ) * g) . s2 in the
carrier of
I[01] )
by A10, A12, FUNCT_2:7;
then reconsider hg1 =
((h " ) * g) . s19,
hg2 =
((h " ) * g) . s29 as
Real by BORSUK_1:83;
A24:
dom g = [#] I[01]
by A2, TOPS_2:def 5;
then A25:
0 in dom g
by BORSUK_1:86;
A26:
dom h = [#] I[01]
by A15, TOPS_2:def 5;
then A27:
t1 in dom h
by A19, BORSUK_1:86;
A28:
0 in dom h
by A26, BORSUK_1:86;
A29:
rng h = [#] ((TOP-REAL 2) | P)
by A15, TOPS_2:def 5;
then (h " ) . p1 =
(h " ) . p1
by A22, TOPS_2:def 4
.=
0
by A16, A28, A22, FUNCT_1:54
;
then A30:
((h " ) * g) . 0 = 0
by A3, A25, FUNCT_1:23;
s1 in dom g
by A6, A24, BORSUK_1:86;
then A31:
((h " ) * g) . s1 =
(h " ) . q1
by A5, FUNCT_1:23
.=
(h " ) . q1
by A29, A22, TOPS_2:def 4
.=
t1
by A18, A22, A27, FUNCT_1:54
;
A32:
t2 in dom h
by A21, A26, BORSUK_1:86;
s2 in dom g
by A8, A24, BORSUK_1:86;
then A33:
((h " ) * g) . s2 =
(h " ) . q2
by A7, FUNCT_1:23
.=
(h " ) . q2
by A29, A22, TOPS_2:def 4
.=
t2
by A20, A22, A32, FUNCT_1:54
;
A34:
1
in dom g
by A24, BORSUK_1:86;
A35:
1
in dom h
by A26, BORSUK_1:86;
(h " ) . p2 =
(h " ) . p2
by A29, A22, TOPS_2:def 4
.=
1
by A17, A35, A22, FUNCT_1:54
;
then A36:
((h " ) * g) . 1
= 1
by A4, A34, FUNCT_1:23;
end;
q1 in P
by A11, PRE_TOPC:def 10;
hence
LE q1,q2,P,p1,p2
by A13, A14, Def3; verum