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