let a, b, d, e, s1, s2, t1, t2 be Real; for h being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (d,e)) st h is being_homeomorphism & h . s1 = t1 & h . s2 = t2 & h . b = d & e >= d & t1 >= t2 & s1 in [.a,b.] & s2 in [.a,b.] holds
s1 <= s2
let h be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (d,e)); ( h is being_homeomorphism & h . s1 = t1 & h . s2 = t2 & h . b = d & e >= d & t1 >= t2 & s1 in [.a,b.] & s2 in [.a,b.] implies s1 <= s2 )
assume that
A1:
h is being_homeomorphism
and
A2:
h . s1 = t1
and
A3:
h . s2 = t2
and
A4:
h . b = d
and
A5:
e >= d
and
A6:
t1 >= t2
and
A7:
s1 in [.a,b.]
and
A8:
s2 in [.a,b.]
; s1 <= s2
A9:
s1 <= b
by A7, XXREAL_1:1;
reconsider C = [.d,e.] as non empty Subset of R^1 by A5, TOPMETR:17, XXREAL_1:1;
A10:
R^1 | C = Closed-Interval-TSpace (d,e)
by A5, TOPMETR:19;
A11:
a <= s1
by A7, XXREAL_1:1;
then A12:
the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.]
by A9, TOPMETR:18, XXREAL_0:2;
then reconsider B1 = [.s1,b.] as Subset of (Closed-Interval-TSpace (a,b)) by A11, XXREAL_1:34;
A13: dom h =
[#] (Closed-Interval-TSpace (a,b))
by A1, TOPS_2:def 5
.=
[.a,b.]
by A11, A9, TOPMETR:18, XXREAL_0:2
;
A14:
a <= s2
by A8, XXREAL_1:1;
then reconsider B = [.s2,s1.] as Subset of (Closed-Interval-TSpace (a,b)) by A9, A12, XXREAL_1:34;
reconsider Bb = [.s2,s1.] as Subset of (Closed-Interval-TSpace (a,b)) by A14, A9, A12, XXREAL_1:34;
reconsider f3 = h | Bb as Function of ((Closed-Interval-TSpace (a,b)) | B),(Closed-Interval-TSpace (d,e)) by PRE_TOPC:9;
assume A15:
s1 > s2
; contradiction
then A16:
Closed-Interval-TSpace (s2,s1) = (Closed-Interval-TSpace (a,b)) | B
by A14, A9, TOPMETR:23;
then
f3 is Function of (Closed-Interval-TSpace (s2,s1)),R^1
by A10, JORDAN6:3;
then reconsider f = h | B as Function of (Closed-Interval-TSpace (s2,s1)),R^1 ;
s2 in B
by A15, XXREAL_1:1;
then A17:
f . s2 = t2
by A3, FUNCT_1:49;
set t = (t1 + t2) / 2;
A18:
the carrier of (Closed-Interval-TSpace (d,e)) = [.d,e.]
by A5, TOPMETR:18;
h is one-to-one
by A1, TOPS_2:def 5;
then
t1 <> t2
by A2, A3, A7, A8, A13, A15, FUNCT_1:def 4;
then A19:
t1 > t2
by A6, XXREAL_0:1;
then
t1 + t1 > t1 + t2
by XREAL_1:8;
then A20:
(2 * t1) / 2 > (t1 + t2) / 2
by XREAL_1:74;
dom f = the carrier of (Closed-Interval-TSpace (s2,s1))
by FUNCT_2:def 1;
then
dom f = [.s2,s1.]
by A15, TOPMETR:18;
then
s2 in dom f
by A15, XXREAL_1:1;
then
t2 in rng f3
by A17, FUNCT_1:def 3;
then A21:
d <= t2
by A18, XXREAL_1:1;
t1 + t2 > t2 + t2
by A19, XREAL_1:8;
then A22:
(2 * t2) / 2 < (t1 + t2) / 2
by XREAL_1:74;
then A23:
d < (t1 + t2) / 2
by A21, XXREAL_0:2;
reconsider B1b = [.s1,b.] as Subset of (Closed-Interval-TSpace (a,b)) by A11, A12, XXREAL_1:34;
reconsider f4 = h | B1b as Function of ((Closed-Interval-TSpace (a,b)) | B1),(Closed-Interval-TSpace (d,e)) by PRE_TOPC:9;
A24:
Closed-Interval-TSpace (s1,b) = (Closed-Interval-TSpace (a,b)) | B1
by A11, A9, TOPMETR:23;
then
f4 is Function of (Closed-Interval-TSpace (s1,b)),R^1
by A10, JORDAN6:3;
then reconsider f1 = h | B1 as Function of (Closed-Interval-TSpace (s1,b)),R^1 ;
A25:
h is continuous
by A1, TOPS_2:def 5;
then
f4 is continuous
by TOPMETR:7;
then A26:
f1 is continuous
by A10, A24, JORDAN6:3;
b in B1
by A9, XXREAL_1:1;
then A27:
f1 . b = d
by A4, FUNCT_1:49;
s1 in B1
by A9, XXREAL_1:1;
then A28:
f1 . s1 = t1
by A2, FUNCT_1:49;
s1 < b
by A2, A4, A9, A19, A21, XXREAL_0:1;
then consider r1 being Real such that
A29:
f1 . r1 = (t1 + t2) / 2
and
A30:
s1 < r1
and
A31:
r1 < b
by A20, A26, A28, A27, A23, TOPREAL5:7;
A32:
r1 in B1
by A30, A31, XXREAL_1:1;
s1 in B
by A15, XXREAL_1:1;
then A33:
f . s1 = t1
by A2, FUNCT_1:49;
f3 is continuous
by A25, TOPMETR:7;
then
f is continuous
by A10, A16, JORDAN6:3;
then consider r being Real such that
A34:
f . r = (t1 + t2) / 2
and
A35:
s2 < r
and
A36:
r < s1
by A15, A17, A33, A20, A22, TOPREAL5:6;
A37:
a < r
by A14, A35, XXREAL_0:2;
a < r1
by A11, A30, XXREAL_0:2;
then A38:
r1 in [.a,b.]
by A31, XXREAL_1:1;
A39:
h is one-to-one
by A1, TOPS_2:def 5;
r < b
by A9, A36, XXREAL_0:2;
then A40:
r in [.a,b.]
by A37, XXREAL_1:1;
r in [.s2,s1.]
by A35, A36, XXREAL_1:1;
then h . r =
(t1 + t2) / 2
by A34, FUNCT_1:49
.=
h . r1
by A29, A32, FUNCT_1:49
;
hence
contradiction
by A13, A39, A36, A40, A30, A38, FUNCT_1:def 4; verum