let P be Subset of (TOP-REAL 2); :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: ( 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 A1:
( 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 )
; :: thesis: LE q1,q2,P,p1,p2
then reconsider P' = P as non empty Subset of (TOP-REAL 2) by TOPREAL1:4;
reconsider g = g as Function of I[01] ,((TOP-REAL 2) | P') ;
A2:
s1 in the carrier of I[01]
by A1, BORSUK_1:86;
then A3:
q1 in [#] ((TOP-REAL 2) | P')
by A1, FUNCT_2:7;
A4:
s2 in the carrier of I[01]
by A1, BORSUK_1:86;
then
g . s2 in the carrier of ((TOP-REAL 2) | P')
by FUNCT_2:7;
then A5:
( q1 in P & q2 in P )
by A1, A3, PRE_TOPC:def 10;
now let h be
Function of
I[01] ,
((TOP-REAL 2) | P');
:: thesis: 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;
:: thesis: ( 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 A6:
(
h is
being_homeomorphism &
h . 0 = p1 &
h . 1
= p2 &
h . t1 = q1 &
0 <= t1 &
t1 <= 1 &
h . t2 = q2 &
0 <= t2 &
t2 <= 1 )
;
:: thesis: b2 <= b3set hg =
(h " ) * g;
h " is
being_homeomorphism
by A6, TOPS_2:70;
then A7:
(h " ) * g is
being_homeomorphism
by A1, TOPS_2:71;
A8:
(
dom h = [#] I[01] &
rng h = [#] ((TOP-REAL 2) | P) )
by A6, TOPS_2:def 5;
then A9:
(
0 in dom h & 1
in dom h )
by BORSUK_1:86;
A10:
h is
one-to-one
by A6, TOPS_2:def 5;
A11:
(
(h " ) * g is
continuous &
(h " ) * g is
one-to-one )
by A7, TOPS_2:def 5;
A12:
(h " ) . p1 =
(h " ) . p1
by A8, A10, TOPS_2:def 4
.=
0
by A6, A9, A10, FUNCT_1:54
;
A13:
(h " ) . p2 =
(h " ) . p2
by A8, A10, TOPS_2:def 4
.=
1
by A6, A9, A10, FUNCT_1:54
;
A14:
(
dom g = [#] I[01] &
rng g = [#] ((TOP-REAL 2) | P) )
by A1, TOPS_2:def 5;
then
0 in dom g
by BORSUK_1:86;
then A15:
((h " ) * g) . 0 = 0
by A1, A12, FUNCT_1:23;
1
in dom g
by A14, BORSUK_1:86;
then A16:
((h " ) * g) . 1
= 1
by A1, A13, FUNCT_1:23;
A17:
t1 in dom h
by A6, A8, BORSUK_1:86;
s1 in dom g
by A1, A14, BORSUK_1:86;
then A18:
((h " ) * g) . s1 =
(h " ) . q1
by A1, FUNCT_1:23
.=
(h " ) . q1
by A8, A10, TOPS_2:def 4
.=
t1
by A6, A10, A17, FUNCT_1:54
;
A19:
t2 in dom h
by A6, A8, BORSUK_1:86;
s2 in dom g
by A1, A14, BORSUK_1:86;
then A20:
((h " ) * g) . s2 =
(h " ) . q2
by A1, FUNCT_1:23
.=
(h " ) . q2
by A8, A10, TOPS_2:def 4
.=
t2
by A6, A10, A19, FUNCT_1:54
;
reconsider s1' =
s1,
s2' =
s2 as
Point of
I[01] by A1, BORSUK_1:86;
(
((h " ) * g) . s1 in the
carrier of
I[01] &
((h " ) * g) . s2 in the
carrier of
I[01] )
by A2, A4, FUNCT_2:7;
then reconsider hg1 =
((h " ) * g) . s1',
hg2 =
((h " ) * g) . s2' as
Real by BORSUK_1:83;
end;
hence
LE q1,q2,P,p1,p2
by A5, Def3; :: thesis: verum