let a, b, c, d be real number ; :: thesis:
let p1, p2 be Point of (TOP-REAL 2); :: thesis:
set K = rectangle a,b,c,d;
assume that
A1: a < b and
A2: c < d and
A3: p1 in LSeg |[a,c]|,|[a,d]| and
A4: p2 in LSeg |[a,c]|,|[a,d]| ; :: thesis:
A5: rectangle a,b,c,d is being_simple_closed_curve by A1, A2, Th60;
A6: p1 `1 = a by A2, A3, Th9;
A7: c <= p1 `2 by A2, A3, Th9;
A8: p2 `1 = a by A2, A4, Th9;
A9: E-max (rectangle a,b,c,d) = |[b,d]| by A1, A2, Th56;
A10: Upper_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) by A1, A2, Th61;
then A11: LSeg |[a,c]|,|[a,d]| c= Upper_Arc (rectangle a,b,c,d) by XBOOLE_1:7;
A12: (Upper_Arc (rectangle a,b,c,d)) /\ (Lower_Arc (rectangle a,b,c,d)) = {(W-min (rectangle a,b,c,d)),(E-max (rectangle a,b,c,d))} by A5, JORDAN6:def 9;

A13: now

assume p2 in Lower_Arc (rectangle a,b,c,d) ; :: thesis:
then A14: p2 in (Upper_Arc (rectangle a,b,c,d)) /\ (Lower_Arc (rectangle a,b,c,d)) by A4, A11, XBOOLE_0:def 4;

now

assume p2 = E-max (rectangle a,b,c,d) ; :: thesis:
then p2 `1 = b by A9, EUCLID:56;
hence contradiction by A1, A4, TOPREAL3:17; :: thesis:

end;

hence p2 = W-min (rectangle a,b,c,d) by A12, A14, TARSKI:def 2; :: thesis:

end;

thus ( LE p1,p2, rectangle a,b,c,d implies p1 `2 <= p2 `2 ) :: thesis:

proof

assume LE p1,p2, rectangle a,b,c,d ; :: thesis:
then A15: ( ( p1 in Upper_Arc (rectangle a,b,c,d) & p2 in Lower_Arc (rectangle a,b,c,d) & not p2 = W-min (rectangle a,b,c,d) ) or ( p1 in Upper_Arc (rectangle a,b,c,d) & p2 in Upper_Arc (rectangle a,b,c,d) & LE p1,p2, Upper_Arc (rectangle a,b,c,d), W-min (rectangle a,b,c,d), E-max (rectangle a,b,c,d) ) or ( p1 in Lower_Arc (rectangle a,b,c,d) & p2 in Lower_Arc (rectangle a,b,c,d) & not p2 = W-min (rectangle a,b,c,d) & LE p1,p2, Lower_Arc (rectangle a,b,c,d), E-max (rectangle a,b,c,d), W-min (rectangle a,b,c,d) ) ) by JORDAN6:def 10;
consider f being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) such that
A16: f is being_homeomorphism and
A17: f . 0 = W-min (rectangle a,b,c,d) and
A18: f . 1 = E-max (rectangle a,b,c,d) and
rng f = Upper_Arc (rectangle a,b,c,d) and
for r being Real st r in [.0 ,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) and
for r being Real st r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) and
A19: for p being Point of (TOP-REAL 2) st p in LSeg |[a,c]|,|[a,d]| holds
( 0 <= (((p `2 ) - c) / (d - c)) / 2 & (((p `2 ) - c) / (d - c)) / 2 <= 1 & f . ((((p `2 ) - c) / (d - c)) / 2) = p ) and
for p being Point of (TOP-REAL 2) st p in LSeg |[a,d]|,|[b,d]| holds
( 0 <= ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) & ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) <= 1 & f . (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2)) = p ) by A1, A2, Th63;
reconsider s1 = (((p1 `2 ) - c) / (d - c)) / 2, s2 = (((p2 `2 ) - c) / (d - c)) / 2 as Real ;
A20: f . s1 = p1 by A3, A19;
A21: f . s2 = p2 by A4, A19;
A22: d - c > 0 by A2, XREAL_1:52;
A23: s1 <= 1 by A3, A19;
A24: 0 <= s2 by A4, A19;
s2 <= 1 by A4, A19;
then s1 <= s2 by A13, A15, A16, A17, A18, A20, A21, A23, A24, JORDAN5C:def 3;
then ((((p1 `2 ) - c) / (d - c)) / 2) * 2 <= ((((p2 `2 ) - c) / (d - c)) / 2) * 2 by XREAL_1:66;
then (((p1 `2 ) - c) / (d - c)) * (d - c) <= (((p2 `2 ) - c) / (d - c)) * (d - c) by A22, XREAL_1:66;
then (p1 `2 ) - c <= (((p2 `2 ) - c) / (d - c)) * (d - c) by A22, XCMPLX_1:88;
then (p1 `2 ) - c <= (p2 `2 ) - c by A22, XCMPLX_1:88;
then ((p1 `2 ) - c) + c <= ((p2 `2 ) - c) + c by XREAL_1:9;
hence p1 `2 <= p2 `2 ; :: thesis:

end;

thus ( p1 `2 <= p2 `2 implies LE p1,p2, rectangle a,b,c,d ) :: thesis:

proof

assume A25: p1 `2 <= p2 `2 ; :: thesis:
for g being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d)))
for s1, s2 being Real st g is being_homeomorphism & g . 0 = W-min (rectangle a,b,c,d) & g . 1 = E-max (rectangle a,b,c,d) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2

proof

let g be Function of I[01] ,((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))); :: thesis:
let s1, s2 be Real; :: thesis:
assume that
A26: g is being_homeomorphism and
A27: g . 0 = W-min (rectangle a,b,c,d) and
g . 1 = E-max (rectangle a,b,c,d) and
A28: g . s1 = p1 and
A29: 0 <= s1 and
A30: s1 <= 1 and
A31: g . s2 = p2 and
A32: 0 <= s2 and
A33: s2 <= 1 ; :: thesis:
A34: dom g = the carrier of I[01] by FUNCT_2:def 1;
A35: g is one-to-one by A26, TOPS_2:def 5;
A36: the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) = Upper_Arc (rectangle a,b,c,d) by PRE_TOPC:29;
then reconsider g1 = g as Function of I[01] ,(TOP-REAL 2) by FUNCT_2:9;
g is continuous by A26, TOPS_2:def 5;
then A37: g1 is continuous by PRE_TOPC:56;
reconsider h1 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
reconsider h2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
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 ;
A38: 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:66
.= (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:39;
then A39: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by PRE_TOPC:62;
( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by A38, JGRAPH_2:40;
then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by PRE_TOPC:62;
then consider h being Function of (TOP-REAL 2),R^1 such that
A40: for p being Point of (TOP-REAL 2)
for r1, r2 being real number st hh1 . p = r1 & hh2 . p = r2 holds
h . p = r1 + r2 and
A41: h is continuous by A39, JGRAPH_2:29;
reconsider k = h * g1 as Function of I[01] ,R^1 ;
A42: W-min (rectangle a,b,c,d) = |[a,c]| by A1, A2, Th56;

now

proof

let x1, x2 be set ; :: thesis:
assume that
A61: x1 in dom k and
A62: x2 in dom k and
A63: k . x1 = k . x2 ; :: thesis:
reconsider r1 = x1 as Point of I[01] by A61;
reconsider r2 = x2 as Point of I[01] by A62;
A64: k . x1 = h . (g1 . x1) by A61, FUNCT_1:22
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A40
.= ((g1 . r1) `1 ) + (proj2 . (g1 . r1)) by PSCOMP_1:def 28
.= ((g1 . r1) `1 ) + ((g1 . r1) `2 ) by PSCOMP_1:def 29 ;
A65: k . x2 = h . (g1 . x2) by A62, FUNCT_1:22
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A40
.= ((g1 . r2) `1 ) + (proj2 . (g1 . r2)) by PSCOMP_1:def 28
.= ((g1 . r2) `1 ) + ((g1 . r2) `2 ) by PSCOMP_1:def 29 ;
A66: g . r1 in Upper_Arc (rectangle a,b,c,d) by A36;
A67: g . r2 in Upper_Arc (rectangle a,b,c,d) by A36;
reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A66;
reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A67;

now

per cases by A10, A36, XBOOLE_0:def 3;

case A68: ( g . r1 in LSeg |[a,c]|,|[a,d]| & g . r2 in LSeg |[a,c]|,|[a,d]| ) ; :: thesis:

then A69: gr1 `1 = a by A2, Th9;
gr2 `1 = a by A2, A68, Th9;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A63, A64, A65, A69, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A34, A35, FUNCT_1:def 8; :: thesis:

end;

case A70: ( g . r1 in LSeg |[a,c]|,|[a,d]| & g . r2 in LSeg |[a,d]|,|[b,d]| ) ; :: thesis:

then A71: gr1 `1 = a by A2, Th9;
A72: gr1 `2 <= d by A2, A70, Th9;
A73: gr2 `2 = d by A1, A70, Th11;
A74: a <= gr2 `1 by A1, A70, Th11;
A75: a + (gr1 `2 ) = (gr2 `1 ) + d by A1, A63, A64, A65, A70, A71, Th11;

A76: now

assume a <> gr2 `1 ; :: thesis:
then a < gr2 `1 by A74, XXREAL_0:1;
hence contradiction by A72, A75, XREAL_1:10; :: thesis:

end;

now

assume gr1 `2 <> d ; :: thesis:
then d > gr1 `2 by A72, XXREAL_0:1;
hence contradiction by A63, A64, A65, A71, A73, A74, XREAL_1:10; :: thesis:

end;

then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A71, A73, A76, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A34, A35, FUNCT_1:def 8; :: thesis:

end;

case A77: ( g . r1 in LSeg |[a,d]|,|[b,d]| & g . r2 in LSeg |[a,c]|,|[a,d]| ) ; :: thesis:

then A78: gr2 `1 = a by A2, Th9;
A79: gr2 `2 <= d by A2, A77, Th9;
A80: gr1 `2 = d by A1, A77, Th11;
A81: a <= gr1 `1 by A1, A77, Th11;
A82: a + (gr2 `2 ) = (gr1 `1 ) + d by A1, A63, A64, A65, A77, A78, Th11;

A83: now

assume a <> gr1 `1 ; :: thesis:
then a < gr1 `1 by A81, XXREAL_0:1;
hence contradiction by A79, A82, XREAL_1:10; :: thesis:

end;

now

assume gr2 `2 <> d ; :: thesis:
then d > gr2 `2 by A79, XXREAL_0:1;
hence contradiction by A63, A64, A65, A78, A80, A81, XREAL_1:10; :: thesis:

end;

then |[(gr2 `1 ),(gr2 `2 )]| = g . r1 by A78, A80, A83, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A34, A35, FUNCT_1:def 8; :: thesis:

end;

case A84: ( g . r1 in LSeg |[a,d]|,|[b,d]| & g . r2 in LSeg |[a,d]|,|[b,d]| ) ; :: thesis:

then A85: gr1 `2 = d by A1, Th11;
gr2 `2 = d by A1, A84, Th11;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A63, A64, A65, A85, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A34, A35, FUNCT_1:def 8; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

A86: dom k = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then s1 in dom k by A29, A30, XXREAL_1:1;
then rxc = s1 by A52, A58, A59, A60, A86;
hence contradiction by A43, A58, XXREAL_1:1; :: thesis:

end;

hence s1 <= s2 ; :: thesis:

end;

then LE p1,p2, Upper_Arc (rectangle a,b,c,d), W-min (rectangle a,b,c,d), E-max (rectangle a,b,c,d) by A3, A4, A11, JORDAN5C:def 3;
hence LE p1,p2, rectangle a,b,c,d by A3, A4, A11, JORDAN6:def 10; :: thesis:

end;