let a, b, c, d be Real; :: 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]|) ; :: thesis:
A4: rectangle (a,b,c,d) is being_simple_closed_curve by A1, A2, Th50;
Upper_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) by A1, A2, Th51;
then A5: LSeg (|[a,c]|,|[a,d]|) c= Upper_Arc (rectangle (a,b,c,d)) by XBOOLE_1:7;
A6: p1 `1 = a by A2, A3, Th1;
A7: c <= p1 `2 by A2, A3, Th1;
A8: p1 `2 <= d by A2, A3, Th1;
thus ( not LE p1,p2, rectangle (a,b,c,d) or ( p2 in LSeg (|[a,c]|,|[a,d]|) & p1 `2 <= p2 `2 ) or p2 in LSeg (|[a,d]|,|[b,d]|) or p2 in LSeg (|[b,d]|,|[b,c]|) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) :: thesis:

proof

assume A9: LE p1,p2, rectangle (a,b,c,d) ; :: thesis:
then A10: p1 in rectangle (a,b,c,d) by A4, JORDAN7:5;
A11: p2 in rectangle (a,b,c,d) by A4, A9, 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 A11, XBOOLE_0:def 3;
then A12: ( 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 :: thesis:

per cases by A12, XBOOLE_0:def 3;

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

hence ( ( p2 in LSeg (|[a,c]|,|[a,d]|) & p1 `2 <= p2 `2 ) or p2 in LSeg (|[a,d]|,|[b,d]|) or p2 in LSeg (|[b,d]|,|[b,c]|) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) by A1, A2, A3, A9, Th55; :: thesis:

end;

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

end;

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

end;

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

now :: thesis:

per cases ;

case p2 = W-min (rectangle (a,b,c,d)) ; :: thesis:

then LE p2,p1, rectangle (a,b,c,d) by A4, A10, JORDAN7:3;
hence ( ( p2 in LSeg (|[a,c]|,|[a,d]|) & p1 `2 <= p2 `2 ) or p2 in LSeg (|[a,d]|,|[b,d]|) or p2 in LSeg (|[b,d]|,|[b,c]|) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) by A1, A2, A3, A9, Th50, JORDAN6:57; :: thesis:

end;

case p2 <> W-min (rectangle (a,b,c,d)) ; :: thesis:

end;

A14: W-min (rectangle (a,b,c,d)) = |[a,c]| by A1, A2, Th46;
thus ( ( ( p2 in LSeg (|[a,c]|,|[a,d]|) & p1 `2 <= p2 `2 ) or p2 in LSeg (|[a,d]|,|[b,d]|) or p2 in LSeg (|[b,d]|,|[b,c]|) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) implies LE p1,p2, rectangle (a,b,c,d) ) :: thesis:

proof

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

now :: thesis:

per cases by A15;

case ( p2 in LSeg (|[a,c]|,|[a,d]|) & p1 `2 <= p2 `2 ) ; :: thesis:

hence LE p1,p2, rectangle (a,b,c,d) by A1, A2, A3, Th55; :: thesis:

end;

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

then A17: p2 `2 = d by A1, Th3;
A18: a <= p2 `1 by A1, A16, Th3;
A19: Upper_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) by A1, A2, Th51;
then A20: p2 in Upper_Arc (rectangle (a,b,c,d)) by A16, XBOOLE_0:def 3;
A21: p1 in Upper_Arc (rectangle (a,b,c,d)) by A3, A19, XBOOLE_0:def 3;
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
A22: g is being_homeomorphism and
A23: g . 0 = W-min (rectangle (a,b,c,d)) and
g . 1 = E-max (rectangle (a,b,c,d)) and
A24: g . s1 = p1 and
A25: 0 <= s1 and
A26: s1 <= 1 and
A27: g . s2 = p2 and
A28: 0 <= s2 and
A29: s2 <= 1 ; :: thesis:
A30: dom g = the carrier of I[01] by FUNCT_2:def 1;
A31: g is one-to-one by A22, TOPS_2:def 5;
A32: the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) = Upper_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 A22, TOPS_2:def 5;
then A33: 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 ;
A34: 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 A35: 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 A34, 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
A36: 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
A37: h is continuous by A35, JGRAPH_2:19;
reconsider k = h * g1 as Function of I[01],R^1 ;
A38: W-min (rectangle (a,b,c,d)) = |[a,c]| by A1, A2, Th46;

now :: thesis:

proof

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

now :: thesis:

per cases by A19, A32, XBOOLE_0:def 3;

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

then A63: gr1 `1 = a by A2, Th1;
gr2 `1 = a by A2, A62, Th1;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by A57, A58, A59, A63, EUCLID:53;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by A30, A31, FUNCT_1:def 4; :: thesis:

end;

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

then A65: gr1 `1 = a by A2, Th1;
A66: gr1 `2 <= d by A2, A64, Th1;
A67: gr2 `2 = d by A1, A64, Th3;
A68: a <= gr2 `1 by A1, A64, Th3;
A69: a + (gr1 `2) = (gr2 `1) + d by A1, A57, A58, A59, A64, A65, Th3;

A70: now :: thesis:

assume a <> gr2 `1 ; :: thesis:
then a < gr2 `1 by A68, XXREAL_0:1;
hence contradiction by A66, A69, XREAL_1:8; :: thesis:

end;

now :: thesis:

assume gr1 `2 <> d ; :: thesis:
then d > gr1 `2 by A66, XXREAL_0:1;
hence contradiction by A57, A58, A59, A65, A67, A68, XREAL_1:8; :: thesis:

end;

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A65, A67, A70, EUCLID:53;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by A30, A31, FUNCT_1:def 4; :: thesis:

end;

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

then A72: gr2 `1 = a by A2, Th1;
A73: gr2 `2 <= d by A2, A71, Th1;
A74: gr1 `2 = d by A1, A71, Th3;
A75: a <= gr1 `1 by A1, A71, Th3;
A76: a + (gr2 `2) = (gr1 `1) + d by A1, A57, A58, A59, A71, A72, Th3;

A77: now :: thesis:

assume a <> gr1 `1 ; :: thesis:
then a < gr1 `1 by A75, XXREAL_0:1;
hence contradiction by A73, A76, XREAL_1:8; :: thesis:

end;

now :: thesis:

assume gr2 `2 <> d ; :: thesis:
then d > gr2 `2 by A73, XXREAL_0:1;
hence contradiction by A57, A58, A59, A72, A74, A75, XREAL_1:8; :: thesis:

end;

then |[(gr2 `1),(gr2 `2)]| = g . r1 by A72, A74, A77, EUCLID:53;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by A30, A31, FUNCT_1:def 4; :: thesis:

end;

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

then A79: gr1 `2 = d by A1, Th3;
gr2 `2 = d by A1, A78, Th3;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by A57, A58, A59, A79, EUCLID:53;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by A30, A31, FUNCT_1:def 4; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

A80: dom k = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then s1 in dom k by A25, A26, XXREAL_1:1;
then rxc = s1 by A48, A52, A53, A54, A80;
hence contradiction by A39, A52, 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 A20, A21, JORDAN5C:def 3;
hence LE p1,p2, rectangle (a,b,c,d) by A20, A21, JORDAN6:def 10; :: thesis:

end;

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

then A82: p2 `1 = b by TOPREAL3:11;
Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[b,d]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[a,c]|)) by A1, A2, Th52;
then A83: LSeg (|[b,d]|,|[b,c]|) c= Lower_Arc (rectangle (a,b,c,d)) by XBOOLE_1:7;
p2 <> W-min (rectangle (a,b,c,d)) by A1, A14, A82, EUCLID:52;
hence LE p1,p2, rectangle (a,b,c,d) by A3, A5, A81, A83, JORDAN6:def 10; :: thesis:

end;

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

Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[b,d]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[a,c]|)) by A1, A2, Th52;
then LSeg (|[b,c]|,|[a,c]|) c= Lower_Arc (rectangle (a,b,c,d)) by XBOOLE_1:7;
hence LE p1,p2, rectangle (a,b,c,d) by A3, A5, A84, JORDAN6:def 10; :: thesis:

end;

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

end;