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

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

then LE p2,p1, rectangle a,b,c,d by A1, Th69;
hence ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) by A1, A4, 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, Th70;
hence ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) by A1, A4, 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, Th71;
hence ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) by A1, A4, 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, A4, 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 A7: ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) ; :: thesis:

now

per cases by A7;

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

then A9: ( p2 `2 = c & a <= p2 `1 & p2 `1 <= b ) by A1, Th11;
A10: Lower_Arc (rectangle a,b,c,d) = (LSeg |[b,d]|,|[b,c]|) \/ (LSeg |[b,c]|,|[a,c]|) by A1, Th62;
then A11: p2 in Lower_Arc (rectangle a,b,c,d) by A8, XBOOLE_0:def 3;
A12: p1 in Lower_Arc (rectangle a,b,c,d) by A1, A10, XBOOLE_0:def 3;
LE p1,p2, Lower_Arc (rectangle a,b,c,d), E-max (rectangle a,b,c,d), W-min (rectangle a,b,c,d)

proof

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 A13: ( 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 ) ; :: thesis:
A14: dom g = the carrier of I[01] by FUNCT_2:def 1;
A15: g is one-to-one by A13, TOPS_2:def 5;
A16: 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 A13, TOPS_2:def 5;
then A17: 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 ;
A18: 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 B24: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies hh1 is continuous ) by JGRAPH_2:39;
A19: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by B24, PRE_TOPC:62;
BB: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by A18, JGRAPH_2:40;
( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by BB, PRE_TOPC:62;
then consider h being Function of (TOP-REAL 2),R^1 such that
A20: ( ( 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 ) & h is continuous ) by A19, JGRAPH_2:29;
reconsider k = h * g1 as Function of I[01] ,R^1 ;
A21: k is continuous Function of I[01] ,R^1 by A17, A20;
A22: E-max (rectangle a,b,c,d) = |[b,d]| by A1, Th56;

now

assume A23: s1 > s2 ; :: thesis:
A24: dom g = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
0 in [.0 ,1.] by XXREAL_1:1;
then A25: k . 0 = h . (E-max (rectangle a,b,c,d)) by A13, A24, FUNCT_1:23
.= (h1 . (E-max (rectangle a,b,c,d))) + (h2 . (E-max (rectangle a,b,c,d))) by A20
.= ((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 A22, EUCLID:56
.= b + d by A22, EUCLID:56 ;
s1 in [.0 ,1.] by A13, XXREAL_1:1;
then A26: k . s1 = h . p1 by A13, A24, FUNCT_1:23
.= (proj1 . p1) + (proj2 . p1) by A20
.= (p1 `1 ) + (proj2 . p1) by PSCOMP_1:def 28
.= (p1 `1 ) + c by A3, PSCOMP_1:def 29 ;
A27: s2 in [.0 ,1.] by A13, XXREAL_1:1;
then k . s2 = h . p2 by A13, A24, FUNCT_1:23
.= (proj1 . p2) + (proj2 . p2) by A20
.= (p2 `1 ) + (proj2 . p2) by PSCOMP_1:def 28
.= (p2 `1 ) + c by A9, PSCOMP_1:def 29 ;
then A28: ( k . 0 >= k . s1 & k . s1 >= k . s2 ) by A1, A3, A8, A25, A26, XREAL_1:9;
A29: 0 in [.0 ,1.] by XXREAL_1:1;
then A30: [.0 ,s2.] c= [.0 ,1.] by A27, XXREAL_2:def 12;
reconsider B = [.0 ,s2.] as Subset of I[01] by A27, A29, BORSUK_1:83, XXREAL_2:def 12;
A31: B is connected by A13, A27, A29, BORSUK_1:83, BORSUK_4:49;
A32: 0 in B by A13, XXREAL_1:1;
A33: s2 in B by A13, XXREAL_1:1;
A34: k . 0 is Real by XREAL_0:def 1;
A35: 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
A36: ( xc in B & k . xc = k . s1 ) by A21, A28, A31, A32, A33, A34, A35, TOPREAL5:11;
xc in [.0 ,1.] by BORSUK_1:83;
then reconsider rxc = xc as Real ;
A37: k is one-to-one

proof

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 A38: ( x1 in dom k & x2 in dom k & k . x1 = k . x2 ) ; :: thesis:
then reconsider r1 = x1 as Point of I[01] ;
reconsider r2 = x2 as Point of I[01] by A38;
A39: k . x1 = h . (g1 . x1) by A38, FUNCT_1:22
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A20
.= ((g1 . r1) `1 ) + (proj2 . (g1 . r1)) by PSCOMP_1:def 28
.= ((g1 . r1) `1 ) + ((g1 . r1) `2 ) by PSCOMP_1:def 29 ;
A40: k . x2 = h . (g1 . x2) by A38, FUNCT_1:22
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A20
.= ((g1 . r2) `1 ) + (proj2 . (g1 . r2)) by PSCOMP_1:def 28
.= ((g1 . r2) `1 ) + ((g1 . r2) `2 ) by PSCOMP_1:def 29 ;
A41: g . r1 in Lower_Arc (rectangle a,b,c,d) by A16;
A42: g . r2 in Lower_Arc (rectangle a,b,c,d) by A16;
reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A41;
reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A42;

now

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

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

then A44: ( gr1 `1 = b & c <= gr1 `2 & gr1 `2 <= d ) by A1, Th9;
( gr2 `1 = b & c <= gr2 `2 & gr2 `2 <= d ) by A1, A43, Th9;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A38, A39, A40, A44, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A14, A15, FUNCT_1:def 8; :: thesis:

end;

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

then A46: ( gr1 `1 = b & c <= gr1 `2 & gr1 `2 <= d ) by A1, Th9;
A47: ( gr2 `2 = c & a <= gr2 `1 & gr2 `1 <= b ) by A1, A45, Th11;
then A48: b + (gr1 `2 ) = (gr2 `1 ) + c by A1, A38, A39, A40, A45, Th9;

A49: now

assume b <> gr2 `1 ; :: thesis:
then b > gr2 `1 by A47, XXREAL_0:1;
hence contradiction by A38, A39, A40, A46, A47, XREAL_1:10; :: thesis:

end;

now

assume gr1 `2 <> c ; :: thesis:
then c < gr1 `2 by A46, XXREAL_0:1;
hence contradiction by A47, A48, XREAL_1:10; :: thesis:

end;

then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A46, A47, A49, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A14, A15, FUNCT_1:def 8; :: thesis:

end;

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

then A51: ( gr2 `1 = b & c <= gr2 `2 & gr2 `2 <= d ) by A1, Th9;
A52: ( gr1 `2 = c & a <= gr1 `1 & gr1 `1 <= b ) by A1, A50, Th11;
A53: b + (gr2 `2 ) = (gr1 `1 ) + c by A1, A38, A39, A40, A50, A51, Th11;

A54: now

assume b <> gr1 `1 ; :: thesis:
then b > gr1 `1 by A52, XXREAL_0:1;
hence contradiction by A51, A53, XREAL_1:10; :: thesis:

end;

now

assume gr2 `2 <> c ; :: thesis:
then c < gr2 `2 by A51, XXREAL_0:1;
hence contradiction by A38, A39, A40, A51, A52, XREAL_1:10; :: thesis:

end;

then |[(gr2 `1 ),(gr2 `2 )]| = g . r1 by A51, A52, A54, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A14, A15, FUNCT_1:def 8; :: thesis:

end;

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

then A56: ( gr1 `2 = c & a <= gr1 `1 & gr1 `1 <= b ) by A1, Th11;
( gr2 `2 = c & a <= gr2 `1 & gr2 `1 <= b ) by A1, A55, Th11;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A38, A39, A40, A56, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A14, A15, FUNCT_1:def 8; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

hence k is one-to-one by FUNCT_1:def 8; :: thesis:

end;

A57: dom k = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then s1 in dom k by A13, XXREAL_1:1;
then rxc = s1 by A30, A36, A37, A57, FUNCT_1:def 8;
hence contradiction by A23, A36, XXREAL_1:1; :: thesis:

end;

hence s1 <= s2 ; :: thesis:

end;

hence 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 A11, A12, JORDAN5C:def 3; :: thesis:

end;

hence LE p1,p2, rectangle a,b,c,d by A7, A11, A12, JORDAN6:def 10; :: thesis:

end;

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

then A59: ( p2 `2 = c & a <= p2 `1 & p2 `1 <= b ) by A1, Th11;
A60: Lower_Arc (rectangle a,b,c,d) = (LSeg |[b,d]|,|[b,c]|) \/ (LSeg |[b,c]|,|[a,c]|) by A1, Th62;
then A61: p2 in Lower_Arc (rectangle a,b,c,d) by A58, XBOOLE_0:def 3;
A62: p1 in Lower_Arc (rectangle a,b,c,d) by A1, A60, XBOOLE_0:def 3;
LE p1,p2, Lower_Arc (rectangle a,b,c,d), E-max (rectangle a,b,c,d), W-min (rectangle a,b,c,d)

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 A63: ( 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 ) ; :: thesis:
A64: dom g = the carrier of I[01] by FUNCT_2:def 1;
A65: g is one-to-one by A63, TOPS_2:def 5;
A66: 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 A63, TOPS_2:def 5;
then A67: 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 ;
A68: 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 B24: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies hh1 is continuous ) by JGRAPH_2:39;
A69: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by B24, PRE_TOPC:62;
BB: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by A68, JGRAPH_2:40;
( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by BB, PRE_TOPC:62;
then consider h being Function of (TOP-REAL 2),R^1 such that
A70: ( ( 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 ) & h is continuous ) by A69, JGRAPH_2:29;
reconsider k = h * g1 as Function of I[01] ,R^1 ;
A71: k is continuous Function of I[01] ,R^1 by A67, A70;
A72: E-max (rectangle a,b,c,d) = |[b,d]| by A1, Th56;

now

assume A73: s1 > s2 ; :: thesis:
A74: dom g = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
0 in [.0 ,1.] by XXREAL_1:1;
then A75: k . 0 = h . (E-max (rectangle a,b,c,d)) by A63, A74, FUNCT_1:23
.= (h1 . (E-max (rectangle a,b,c,d))) + (h2 . (E-max (rectangle a,b,c,d))) by A70
.= ((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 A72, EUCLID:56
.= b + d by A72, EUCLID:56 ;
s1 in [.0 ,1.] by A63, XXREAL_1:1;
then A76: k . s1 = h . p1 by A63, A74, FUNCT_1:23
.= (proj1 . p1) + (proj2 . p1) by A70
.= (p1 `1 ) + (proj2 . p1) by PSCOMP_1:def 28
.= (p1 `1 ) + c by A3, PSCOMP_1:def 29 ;
A77: s2 in [.0 ,1.] by A63, XXREAL_1:1;
then k . s2 = h . p2 by A63, A74, FUNCT_1:23
.= (proj1 . p2) + (proj2 . p2) by A70
.= (p2 `1 ) + (proj2 . p2) by PSCOMP_1:def 28
.= (p2 `1 ) + c by A59, PSCOMP_1:def 29 ;
then A78: ( k . 0 >= k . s1 & k . s1 >= k . s2 ) by A1, A3, A7, A75, A76, XREAL_1:9;
A79: 0 in [.0 ,1.] by XXREAL_1:1;
then A80: [.0 ,s2.] c= [.0 ,1.] by A77, XXREAL_2:def 12;
reconsider B = [.0 ,s2.] as Subset of I[01] by A77, A79, BORSUK_1:83, XXREAL_2:def 12;
A81: B is connected by A63, A77, A79, BORSUK_1:83, BORSUK_4:49;
A82: 0 in B by A63, XXREAL_1:1;
A83: s2 in B by A63, XXREAL_1:1;
A84: k . 0 is Real by XREAL_0:def 1;
A85: 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
A86: ( xc in B & k . xc = k . s1 ) by A71, A78, A81, A82, A83, A84, A85, TOPREAL5:11;
xc in [.0 ,1.] by BORSUK_1:83;
then reconsider rxc = xc as Real ;
A87: k is one-to-one

proof

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 A88: ( x1 in dom k & x2 in dom k & k . x1 = k . x2 ) ; :: thesis:
then reconsider r1 = x1 as Point of I[01] ;
reconsider r2 = x2 as Point of I[01] by A88;
A89: k . x1 = h . (g1 . x1) by A88, FUNCT_1:22
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A70
.= ((g1 . r1) `1 ) + (proj2 . (g1 . r1)) by PSCOMP_1:def 28
.= ((g1 . r1) `1 ) + ((g1 . r1) `2 ) by PSCOMP_1:def 29 ;
A90: k . x2 = h . (g1 . x2) by A88, FUNCT_1:22
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A70
.= ((g1 . r2) `1 ) + (proj2 . (g1 . r2)) by PSCOMP_1:def 28
.= ((g1 . r2) `1 ) + ((g1 . r2) `2 ) by PSCOMP_1:def 29 ;
A91: g . r1 in Lower_Arc (rectangle a,b,c,d) by A66;
A92: g . r2 in Lower_Arc (rectangle a,b,c,d) by A66;
reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A91;
reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A92;

now

per cases by A60, A66, XBOOLE_0:def 3;

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

then A94: ( gr1 `1 = b & c <= gr1 `2 & gr1 `2 <= d ) by A1, Th9;
( gr2 `1 = b & c <= gr2 `2 & gr2 `2 <= d ) by A1, A93, Th9;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A88, A89, A90, A94, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A64, A65, FUNCT_1:def 8; :: thesis:

end;

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

then A96: ( gr1 `1 = b & c <= gr1 `2 & gr1 `2 <= d ) by A1, Th9;
A97: ( gr2 `2 = c & a <= gr2 `1 & gr2 `1 <= b ) by A1, A95, Th11;
then A98: b + (gr1 `2 ) = (gr2 `1 ) + c by A1, A88, A89, A90, A95, Th9;

A99: now

assume b <> gr2 `1 ; :: thesis:
then b > gr2 `1 by A97, XXREAL_0:1;
hence contradiction by A88, A89, A90, A96, A97, XREAL_1:10; :: thesis:

end;

now

assume gr1 `2 <> c ; :: thesis:
then c < gr1 `2 by A96, XXREAL_0:1;
hence contradiction by A97, A98, XREAL_1:10; :: thesis:

end;

then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A96, A97, A99, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A64, A65, FUNCT_1:def 8; :: thesis:

end;

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

then A101: ( gr2 `1 = b & c <= gr2 `2 & gr2 `2 <= d ) by A1, Th9;
A102: ( gr1 `2 = c & a <= gr1 `1 & gr1 `1 <= b ) by A1, A100, Th11;
A103: b + (gr2 `2 ) = (gr1 `1 ) + c by A1, A88, A89, A90, A100, A101, Th11;

A104: now

assume b <> gr1 `1 ; :: thesis:
then b > gr1 `1 by A102, XXREAL_0:1;
hence contradiction by A101, A103, XREAL_1:10; :: thesis:

end;

now

assume gr2 `2 <> c ; :: thesis:
then c < gr2 `2 by A101, XXREAL_0:1;
hence contradiction by A88, A89, A90, A101, A102, XREAL_1:10; :: thesis:

end;

then |[(gr2 `1 ),(gr2 `2 )]| = g . r1 by A101, A102, A104, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A64, A65, FUNCT_1:def 8; :: thesis:

end;

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

then A106: ( gr1 `2 = c & a <= gr1 `1 & gr1 `1 <= b ) by A1, Th11;
( gr2 `2 = c & a <= gr2 `1 & gr2 `1 <= b ) by A1, A105, Th11;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A88, A89, A90, A106, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A64, A65, FUNCT_1:def 8; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

hence k is one-to-one by FUNCT_1:def 8; :: thesis:

end;

A107: dom k = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then s1 in dom k by A63, XXREAL_1:1;
then rxc = s1 by A80, A86, A87, A107, FUNCT_1:def 8;
hence contradiction by A73, A86, XXREAL_1:1; :: thesis:

end;

hence s1 <= s2 ; :: thesis:

end;

hence 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 A61, A62, JORDAN5C:def 3; :: thesis:

end;

hence LE p1,p2, rectangle a,b,c,d by A58, A61, A62, JORDAN6:def 10; :: thesis:

end;

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

end;