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 |[b,c]|,|[a,c]| and
A4: p1 <> W-min (rectangle a,b,c,d) ; :: thesis:
A5: rectangle a,b,c,d is being_simple_closed_curve by A1, A2, Th60;
A6: p1 `2 = c by A1, A3, Th11;
A7: p1 `1 <= b by A1, A3, Th11;
thus ( LE p1,p2, rectangle a,b,c,d implies ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) ) :: thesis:

proof

assume A8: LE p1,p2, rectangle a,b,c,d ; :: thesis:
then A9: p2 in rectangle a,b,c,d by A5, JORDAN7:5;
rectangle a,b,c,d = ((LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|)) \/ ((LSeg |[a,c]|,|[b,c]|) \/ (LSeg |[b,c]|,|[b,d]|)) by SPPOL_2:def 3
.= (((LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|)) \/ (LSeg |[b,d]|,|[b,c]|)) \/ (LSeg |[b,c]|,|[a,c]|) by XBOOLE_1:4 ;
then ( p2 in ((LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|)) \/ (LSeg |[b,d]|,|[b,c]|) or p2 in LSeg |[b,c]|,|[a,c]| ) by A9, XBOOLE_0:def 3;
then A10: ( p2 in (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) or p2 in LSeg |[b,d]|,|[b,c]| or p2 in LSeg |[b,c]|,|[a,c]| ) by XBOOLE_0:def 3;

now

per cases by A10, XBOOLE_0:def 3;

case p2 in LSeg |[a,c]|,|[a,d]| ; :: thesis:

then LE p2,p1, rectangle a,b,c,d by A1, A2, A3, A4, Th69;
hence ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) by A1, A2, A3, A4, A8, Th60, JORDAN6:72; :: thesis:

end;

case p2 in LSeg |[a,d]|,|[b,d]| ; :: thesis:

then LE p2,p1, rectangle a,b,c,d by A1, A2, A3, A4, Th70;
hence ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) by A1, A2, A3, A4, A8, Th60, JORDAN6:72; :: thesis:

end;

case p2 in LSeg |[b,d]|,|[b,c]| ; :: thesis:

then LE p2,p1, rectangle a,b,c,d by A1, A2, A3, A4, Th71;
hence ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) by A1, A2, A3, A4, A8, Th60, JORDAN6:72; :: thesis:

end;

case p2 in LSeg |[b,c]|,|[a,c]| ; :: thesis:

hence ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) by A1, A2, A3, A4, A8, Th68; :: thesis:

end;

hence ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) ; :: thesis:

end;

thus ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) implies LE p1,p2, rectangle a,b,c,d ) :: thesis:

proof

assume that
A11: p2 in LSeg |[b,c]|,|[a,c]| and
A12: p1 `1 >= p2 `1 and
A13: p2 <> W-min (rectangle a,b,c,d) ; :: thesis:

now

per cases by A11, A12;

case A14: ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 ) ; :: thesis:

then A15: p2 `2 = c by A1, Th11;
A16: Lower_Arc (rectangle a,b,c,d) = (LSeg |[b,d]|,|[b,c]|) \/ (LSeg |[b,c]|,|[a,c]|) by A1, A2, Th62;
then A17: p2 in Lower_Arc (rectangle a,b,c,d) by A14, XBOOLE_0:def 3;
A18: p1 in Lower_Arc (rectangle a,b,c,d) by A3, A16, XBOOLE_0:def 3;
for g being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d)))
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

proof

let g be Function of I[01] ,((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d))); :: thesis:
let s1, s2 be Real; :: thesis:
assume that
A19: g is being_homeomorphism and
A20: g . 0 = E-max (rectangle a,b,c,d) and
g . 1 = W-min (rectangle a,b,c,d) and
A21: g . s1 = p1 and
A22: 0 <= s1 and
A23: s1 <= 1 and
A24: g . s2 = p2 and
A25: 0 <= s2 and
A26: s2 <= 1 ; :: thesis:
A27: dom g = the carrier of I[01] by FUNCT_2:def 1;
A28: g is one-to-one by A19, TOPS_2:def 5;
A29: the carrier of ((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d))) = Lower_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 A19, TOPS_2:def 5;
then A30: 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 ;
A31: 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 A32: ( ( 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 A31, 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
A33: for p being Point of (TOP-REAL 2)
for r1, r2 being real number st h1 . p = r1 & h2 . p = r2 holds
h . p = r1 + r2 and
A34: h is continuous by A32, JGRAPH_2:29;
reconsider k = h * g1 as Function of I[01] ,R^1 ;
A35: E-max (rectangle a,b,c,d) = |[b,d]| by A1, A2, Th56;

now

assume A36: s1 > s2 ; :: thesis:
A37: dom g = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
0 in [.0 ,1.] by XXREAL_1:1;
then A38: k . 0 = h . (E-max (rectangle a,b,c,d)) by A20, A37, FUNCT_1:23
.= (h1 . (E-max (rectangle a,b,c,d))) + (h2 . (E-max (rectangle a,b,c,d))) by A33
.= ((E-max (rectangle a,b,c,d)) `1 ) + (proj2 . (E-max (rectangle a,b,c,d))) by PSCOMP_1:def 28
.= ((E-max (rectangle a,b,c,d)) `1 ) + ((E-max (rectangle a,b,c,d)) `2 ) by PSCOMP_1:def 29
.= ((E-max (rectangle a,b,c,d)) `1 ) + d by A35, EUCLID:56
.= b + d by A35, EUCLID:56 ;
s1 in [.0 ,1.] by A22, A23, XXREAL_1:1;
then A39: k . s1 = h . p1 by A21, A37, FUNCT_1:23
.= (proj1 . p1) + (proj2 . p1) by A33
.= (p1 `1 ) + (proj2 . p1) by PSCOMP_1:def 28
.= (p1 `1 ) + c by A6, PSCOMP_1:def 29 ;
A40: s2 in [.0 ,1.] by A25, A26, XXREAL_1:1;
then A41: k . s2 = h . p2 by A24, A37, FUNCT_1:23
.= (proj1 . p2) + (proj2 . p2) by A33
.= (p2 `1 ) + (proj2 . p2) by PSCOMP_1:def 28
.= (p2 `1 ) + c by A15, PSCOMP_1:def 29 ;
A42: k . 0 >= k . s1 by A2, A7, A38, A39, XREAL_1:9;
A43: k . s1 >= k . s2 by A14, A39, A41, XREAL_1:9;
A44: 0 in [.0 ,1.] by XXREAL_1:1;
then A45: [.0 ,s2.] c= [.0 ,1.] by A40, XXREAL_2:def 12;
reconsider B = [.0 ,s2.] as Subset of I[01] by A40, A44, BORSUK_1:83, XXREAL_2:def 12;
A46: B is connected by A25, A40, A44, BORSUK_1:83, BORSUK_4:49;
A47: 0 in B by A25, XXREAL_1:1;
A48: s2 in B by A25, XXREAL_1:1;
A49: k . 0 is Real by XREAL_0:def 1;
A50: k . s2 is Real by XREAL_0:def 1;
k . s1 is Real by XREAL_0:def 1;
then consider xc being Point of I[01] such that
A51: xc in B and
A52: k . xc = k . s1 by A30, A34, A42, A43, A46, A47, A48, A49, A50, TOPREAL5:11;
xc in [.0 ,1.] by BORSUK_1:83;
then reconsider rxc = xc as Real ;
A53: for x1, x2 being set st x1 in dom k & x2 in dom k & k . x1 = k . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis:
assume that
A54: x1 in dom k and
A55: x2 in dom k and
A56: k . x1 = k . x2 ; :: thesis:
reconsider r1 = x1 as Point of I[01] by A54;
reconsider r2 = x2 as Point of I[01] by A55;
A57: k . x1 = h . (g1 . x1) by A54, FUNCT_1:22
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A33
.= ((g1 . r1) `1 ) + (proj2 . (g1 . r1)) by PSCOMP_1:def 28
.= ((g1 . r1) `1 ) + ((g1 . r1) `2 ) by PSCOMP_1:def 29 ;
A58: k . x2 = h . (g1 . x2) by A55, FUNCT_1:22
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A33
.= ((g1 . r2) `1 ) + (proj2 . (g1 . r2)) by PSCOMP_1:def 28
.= ((g1 . r2) `1 ) + ((g1 . r2) `2 ) by PSCOMP_1:def 29 ;
A59: g . r1 in Lower_Arc (rectangle a,b,c,d) by A29;
A60: g . r2 in Lower_Arc (rectangle a,b,c,d) by A29;
reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A59;
reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A60;

now

per cases by A16, A29, XBOOLE_0:def 3;

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

then A62: gr1 `1 = b by A2, Th9;
gr2 `1 = b by A2, A61, Th9;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A56, A57, A58, A62, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A27, A28, FUNCT_1:def 8; :: thesis:

end;

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

then A64: gr1 `1 = b by A2, Th9;
A65: c <= gr1 `2 by A2, A63, Th9;
A66: gr2 `2 = c by A1, A63, Th11;
A67: gr2 `1 <= b by A1, A63, Th11;
A68: b + (gr1 `2 ) = (gr2 `1 ) + c by A2, A56, A57, A58, A63, A66, Th9;

A69: now

assume b <> gr2 `1 ; :: thesis:
then b > gr2 `1 by A67, XXREAL_0:1;
hence contradiction by A56, A57, A58, A64, A65, A66, XREAL_1:10; :: thesis:

end;

now

assume gr1 `2 <> c ; :: thesis:
then c < gr1 `2 by A65, XXREAL_0:1;
hence contradiction by A67, A68, XREAL_1:10; :: thesis:

end;

then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A64, A66, A69, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A27, A28, FUNCT_1:def 8; :: thesis:

end;

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

then A71: gr2 `1 = b by A2, Th9;
A72: c <= gr2 `2 by A2, A70, Th9;
A73: gr1 `2 = c by A1, A70, Th11;
A74: gr1 `1 <= b by A1, A70, Th11;
A75: b + (gr2 `2 ) = (gr1 `1 ) + c by A1, A56, A57, A58, A70, A71, Th11;

A76: now

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

end;

now

assume gr2 `2 <> c ; :: thesis:
then c < gr2 `2 by A72, XXREAL_0:1;
hence contradiction by A56, A57, A58, A71, A73, A74, XREAL_1:10; :: thesis:

end;

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

end;

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

then A78: gr1 `2 = c by A1, Th11;
gr2 `2 = c by A1, A77, Th11;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A56, A57, A58, A78, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A27, A28, FUNCT_1:def 8; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

A79: dom k = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then s1 in dom k by A22, A23, XXREAL_1:1;
then rxc = s1 by A45, A51, A52, A53, A79;
hence contradiction by A36, A51, XXREAL_1:1; :: thesis:

end;

hence s1 <= s2 ; :: thesis:

end;

then 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 A17, A18, JORDAN5C:def 3;
hence LE p1,p2, rectangle a,b,c,d by A13, A17, A18, JORDAN6:def 10; :: thesis:

end;

case A80: ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ; :: thesis:

then A81: p2 `2 = c by A1, Th11;
A82: Lower_Arc (rectangle a,b,c,d) = (LSeg |[b,d]|,|[b,c]|) \/ (LSeg |[b,c]|,|[a,c]|) by A1, A2, Th62;
then A83: p2 in Lower_Arc (rectangle a,b,c,d) by A80, XBOOLE_0:def 3;
A84: p1 in Lower_Arc (rectangle a,b,c,d) by A3, A82, XBOOLE_0:def 3;
for g being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d)))
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

proof

let g be Function of I[01] ,((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d))); :: thesis:
let s1, s2 be Real; :: thesis:
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:
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:29;
then reconsider g1 = g as Function of I[01] ,(TOP-REAL 2) by FUNCT_2:9;
g is continuous by A85, TOPS_2:def 5;
then A96: 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 ;
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: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 A98: ( ( 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 A97, 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
A99: for p being Point of (TOP-REAL 2)
for r1, r2 being real number st h1 . p = r1 & h2 . p = r2 holds
h . p = r1 + r2 and
A100: h is continuous by A98, JGRAPH_2:29;
reconsider k = h * g1 as Function of I[01] ,R^1 ;
A101: E-max (rectangle a,b,c,d) = |[b,d]| by A1, A2, Th56;

now

proof

let x1, x2 be set ; :: thesis:
assume that
A120: x1 in dom k and
A121: x2 in dom k and
A122: k . x1 = k . x2 ; :: thesis:
reconsider r1 = x1 as Point of I[01] by A120;
reconsider r2 = x2 as Point of I[01] by A121;
A123: k . x1 = h . (g1 . x1) by A120, FUNCT_1:22
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A99
.= ((g1 . r1) `1 ) + (proj2 . (g1 . r1)) by PSCOMP_1:def 28
.= ((g1 . r1) `1 ) + ((g1 . r1) `2 ) by PSCOMP_1:def 29 ;
A124: k . x2 = h . (g1 . x2) by A121, FUNCT_1:22
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A99
.= ((g1 . r2) `1 ) + (proj2 . (g1 . r2)) by PSCOMP_1:def 28
.= ((g1 . r2) `1 ) + ((g1 . r2) `2 ) by PSCOMP_1:def 29 ;
A125: g . r1 in Lower_Arc (rectangle a,b,c,d) by A95;
A126: g . r2 in Lower_Arc (rectangle a,b,c,d) by A95;
reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A125;
reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A126;

now

per cases by A82, A95, XBOOLE_0:def 3;

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

then A128: gr1 `1 = b by A2, Th9;
gr2 `1 = b by A2, A127, Th9;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A122, A123, A124, A128, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A93, A94, FUNCT_1:def 8; :: thesis:

end;

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

then A130: gr1 `1 = b by A2, Th9;
A131: c <= gr1 `2 by A2, A129, Th9;
A132: gr2 `2 = c by A1, A129, Th11;
A133: gr2 `1 <= b by A1, A129, Th11;
A134: b + (gr1 `2 ) = (gr2 `1 ) + c by A2, A122, A123, A124, A129, A132, Th9;

A135: now

assume b <> gr2 `1 ; :: thesis:
then b > gr2 `1 by A133, XXREAL_0:1;
hence contradiction by A122, A123, A124, A130, A131, A132, XREAL_1:10; :: thesis:

end;

now

assume gr1 `2 <> c ; :: thesis:
then c < gr1 `2 by A131, XXREAL_0:1;
hence contradiction by A133, A134, XREAL_1:10; :: thesis:

end;

then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A130, A132, A135, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A93, A94, FUNCT_1:def 8; :: thesis:

end;

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

then A137: gr2 `1 = b by A2, Th9;
A138: c <= gr2 `2 by A2, A136, Th9;
A139: gr1 `2 = c by A1, A136, Th11;
A140: gr1 `1 <= b by A1, A136, Th11;
A141: b + (gr2 `2 ) = (gr1 `1 ) + c by A1, A122, A123, A124, A136, A137, Th11;

A142: now

assume b <> gr1 `1 ; :: thesis:
then b > gr1 `1 by A140, XXREAL_0:1;
hence contradiction by A138, A141, XREAL_1:10; :: thesis:

end;

now

assume gr2 `2 <> c ; :: thesis:
then c < gr2 `2 by A138, XXREAL_0:1;
hence contradiction by A122, A123, A124, A137, A139, A140, XREAL_1:10; :: thesis:

end;

then |[(gr2 `1 ),(gr2 `2 )]| = g . r1 by A137, A139, A142, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A93, A94, FUNCT_1:def 8; :: thesis:

end;

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

then A144: gr1 `2 = c by A1, Th11;
gr2 `2 = c by A1, A143, Th11;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A122, A123, A124, A144, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A93, A94, FUNCT_1:def 8; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

A145: dom k = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then s1 in dom k by A88, A89, XXREAL_1:1;
then rxc = s1 by A111, A117, A118, A119, A145;
hence contradiction by A102, A117, XXREAL_1:1; :: thesis:

end;

hence s1 <= s2 ; :: thesis:

end;

then 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 A83, A84, JORDAN5C:def 3;
hence LE p1,p2, rectangle a,b,c,d by A80, A83, A84, JORDAN6:def 10; :: thesis:

end;

hence LE p1,p2, rectangle a,b,c,d ; :: thesis:

end;