let g be Function of I[01],((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))); :: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = E-max (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A20: g is being_homeomorphism and
A21: g . 0 = E-max (rectangle (a,b,c,d)) and
g . 1 = W-min (rectangle (a,b,c,d)) and
A22: g . s1 = p1 and
A23: 0 <= s1 and
A24: s1 <= 1 and
A25: g . s2 = p2 and
A26: 0 <= s2 and
A27: s2 <= 1 ; :: thesis: s1 <= s2
A28: dom g = the carrier of I[01] by FUNCT_2:def 1;
A29: g is one-to-one by A20, TOPS_2:def 5;
A30: the carrier of ((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) = Lower_Arc (rectangle (a,b,c,d)) by PRE_TOPC:8;
then reconsider g1 = g as Function of I[01],(TOP-REAL 2) by FUNCT_2:7;
g is continuous by A20, TOPS_2:def 5;
then A31: g1 is continuous by PRE_TOPC:26;
reconsider h1 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
reconsider h2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
reconsider hh1 = h1 as Function of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #),R^1 ;
reconsider hh2 = h2 as Function of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #),R^1 ;
A32: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) | ([#] TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)) by TSEP_1:3
.= TopStruct(# the carrier of ((TOP-REAL 2) | ([#] (TOP-REAL 2))), the topology of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) #) by PRE_TOPC:36
.= (TOP-REAL 2) | ([#] (TOP-REAL 2)) ;
then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies hh1 is continuous ) by JGRAPH_2:29;
then A33: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by PRE_TOPC:32;
( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by A32, JGRAPH_2:30;
then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by PRE_TOPC:32;
then consider h being Function of (TOP-REAL 2),R^1 such that
A34: for p being Point of (TOP-REAL 2)
for r1, r2 being Real st h1 . p = r1 & h2 . p = r2 holds
h . p = r1 + r2 and
A35: h is continuous by A33, JGRAPH_2:19;
reconsider k = h * g1 as Function of I[01],R^1 ;
A36: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;
hence s1 <= s2 ; :: thesis: verum

let g be Function of I[01],((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))); :: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = E-max (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A85: g is being_homeomorphism and
A86: g . 0 = E-max (rectangle (a,b,c,d)) and
g . 1 = W-min (rectangle (a,b,c,d)) and
A87: g . s1 = p1 and
A88: 0 <= s1 and
A89: s1 <= 1 and
A90: g . s2 = p2 and
A91: 0 <= s2 and
A92: s2 <= 1 ; :: thesis: s1 <= s2
A93: dom g = the carrier of I[01] by FUNCT_2:def 1;
A94: g is one-to-one by A85, TOPS_2:def 5;
A95: the carrier of ((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) = Lower_Arc (rectangle (a,b,c,d)) by PRE_TOPC:8;
then reconsider g1 = g as Function of I[01],(TOP-REAL 2) by FUNCT_2:7;
g is continuous by A85, TOPS_2:def 5;
then A96: g1 is continuous by PRE_TOPC:26;
reconsider h1 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
reconsider h2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
reconsider hh1 = h1 as Function of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #),R^1 ;
reconsider hh2 = h2 as Function of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #),R^1 ;
A97: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) | ([#] TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)) by TSEP_1:3
.= TopStruct(# the carrier of ((TOP-REAL 2) | ([#] (TOP-REAL 2))), the topology of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) #) by PRE_TOPC:36
.= (TOP-REAL 2) | ([#] (TOP-REAL 2)) ;
then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies hh1 is continuous ) by JGRAPH_2:29;
then A98: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by PRE_TOPC:32;
( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by A97, JGRAPH_2:30;
then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by PRE_TOPC:32;
then consider h being Function of (TOP-REAL 2),R^1 such that
A99: for p being Point of (TOP-REAL 2)
for r1, r2 being Real st h1 . p = r1 & h2 . p = r2 holds
h . p = r1 + r2 and
A100: h is continuous by A98, JGRAPH_2:19;
reconsider k = h * g1 as Function of I[01],R^1 ;
A101: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;
hence s1 <= s2 ; :: thesis: verum