let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis:
let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis:
set K = rectangle ((- 1),1,(- 1),1);
assume that
A1: P = circle (0,0,1) and
A2: f = Sq_Circ ; :: thesis:
A3: rectangle ((- 1),1,(- 1),1) is being_simple_closed_curve by Th50;
A4: rectangle ((- 1),1,(- 1),1) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } by Lm15;
A5: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } by A1, Th24;
thus ( LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) implies f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) :: thesis:

assume that
A6: LE p1,p2, rectangle ((- 1),1,(- 1),1) and
A7: LE p2,p3, rectangle ((- 1),1,(- 1),1) and
A8: LE p3,p4, rectangle ((- 1),1,(- 1),1) ; :: thesis:
A9: p1 in rectangle ((- 1),1,(- 1),1) by A3, A6, JORDAN7:5;
A10: p2 in rectangle ((- 1),1,(- 1),1) by A3, A6, JORDAN7:5;
A11: p3 in rectangle ((- 1),1,(- 1),1) by A3, A7, JORDAN7:5;
A12: p4 in rectangle ((- 1),1,(- 1),1) by A3, A8, JORDAN7:5;
then A13: ex q8 being Point of (TOP-REAL 2) st
( q8 = p4 & ( ( q8 `1 = - 1 & - 1 <= q8 `2 & q8 `2 <= 1 ) or ( q8 `2 = 1 & - 1 <= q8 `1 & q8 `1 <= 1 ) or ( q8 `1 = 1 & - 1 <= q8 `2 & q8 `2 <= 1 ) or ( q8 `2 = - 1 & - 1 <= q8 `1 & q8 `1 <= 1 ) ) ) by A4;
A14: LE p1,p3, rectangle ((- 1),1,(- 1),1) by A6, A7, Th50, JORDAN6:58;
A15: LE p2,p4, rectangle ((- 1),1,(- 1),1) by A7, A8, Th50, JORDAN6:58;
A16: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;
A17: |[(- 1),0]| `2 = 0 by EUCLID:52;
A18: (1 / 2) * (|[(- 1),(- 1)]| + |[(- 1),1]|) = ((1 / 2) * |[(- 1),(- 1)]|) + ((1 / 2) * |[(- 1),1]|) by RLVECT_1:def 5
.= |[((1 / 2) * (- 1)),((1 / 2) * (- 1))]| + ((1 / 2) * |[(- 1),1]|) by EUCLID:58
.= |[((1 / 2) * (- 1)),((1 / 2) * (- 1))]| + |[((1 / 2) * (- 1)),((1 / 2) * 1)]| by EUCLID:58
.= |[(((1 / 2) * (- 1)) + ((1 / 2) * (- 1))),(((1 / 2) * (- 1)) + ((1 / 2) * 1))]| by EUCLID:56
.= |[(- 1),0]| ;
then A19: |[(- 1),0]| in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by RLTOPSP1:69;

per cases by A9, A16, Th63, RLTOPSP1:68;

case A20: p1 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ; :: thesis:

then A21: p1 `1 = - 1 by Th1;
then A22: (f . p1) `1 < 0 by A2, Th68;
A23: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A24: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A25: f . p1 in P by A9, A23, FUNCT_1:def 6;

now :: thesis:

per cases ;

case A26: p1 `2 >= 0 ; :: thesis:

then A27: LE f . p1,f . p2,P by A1, A2, A6, A20, Th65;
A28: LE f . p2,f . p3,P by A1, A2, A6, A7, A20, A26, Th66;
LE f . p3,f . p4,P by A1, A2, A8, A14, A20, A26, Th66;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A27, A28, JORDAN17:def 1; :: thesis:

end;

case A29: p1 `2 < 0 ; :: thesis:

now :: thesis:

per cases ;

case A30: ( p2 `2 < 0 & p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis:

then A31: p2 `1 = - 1 by Th1;
A32: f . p2 in P by A10, A23, A24, FUNCT_1:def 6;
A33: p1 `2 <= p2 `2 by A6, A20, A30, Th55;

now :: thesis:

per cases ;

case A34: ( p3 `2 < 0 & p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis:

then A35: p3 `1 = - 1 by Th1;
A36: f . p3 in P by A11, A23, A24, FUNCT_1:def 6;
A37: p2 `2 <= p3 `2 by A7, A30, A34, Th55;

now :: thesis:

per cases ;

case A38: ( p4 `2 < 0 & p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis:

then A39: p4 `1 = - 1 by Th1;
A40: (f . p2) `1 < 0 by A2, A30, A31, Th67;
A41: (f . p2) `2 < 0 by A2, A30, A31, Th67;
A42: (f . p3) `1 < 0 by A2, A34, A35, Th67;
A43: (f . p3) `2 < 0 by A2, A34, A35, Th67;
A44: (f . p4) `1 < 0 by A2, A38, A39, Th67;
A45: (f . p4) `2 < 0 by A2, A38, A39, Th67;
(f . p1) `2 <= (f . p2) `2 by A2, A20, A30, A33, Th71;
then A46: LE f . p1,f . p2,P by A5, A22, A25, A32, A40, A41, JGRAPH_5:51;
(f . p2) `2 <= (f . p3) `2 by A2, A30, A34, A37, Th71;
then A47: LE f . p2,f . p3,P by A5, A32, A36, A40, A42, A43, JGRAPH_5:51;
A48: f . p4 in P by A12, A23, A24, FUNCT_1:def 6;
p3 `2 <= p4 `2 by A8, A34, A38, Th55;
then (f . p3) `2 <= (f . p4) `2 by A2, A34, A38, Th71;
then LE f . p3,f . p4,P by A5, A36, A42, A44, A45, A48, JGRAPH_5:51;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A46, A47, JORDAN17:def 1; :: thesis:

end;

case A49: ( not p4 `2 < 0 or not p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis:

A50: now :: thesis:

per cases by A12, Th63;

case p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ; :: thesis:

hence ( ( p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p4 `2 ) or p4 in LSeg (|[(- 1),1]|,|[1,1]|) or p4 in LSeg (|[1,1]|,|[1,(- 1)]|) or ( p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p4 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ) by A49, EUCLID:52; :: thesis:

end;

case p4 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis:

end;

case p4 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis:

end;

case A51: p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis:

A52: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;

now :: thesis:

assume A53: p4 = W-min (rectangle ((- 1),1,(- 1),1)) ; :: thesis:
then p4 `2 = - 1 by A52, EUCLID:52;
hence contradiction by A49, A52, A53, RLTOPSP1:68; :: thesis:

end;

A54: (f . p2) `1 < 0 by A2, A30, A31, Th67;
A55: (f . p2) `2 < 0 by A2, A30, A31, Th67;
A56: (f . p3) `1 < 0 by A2, A34, A35, Th67;
A57: (f . p3) `2 < 0 by A2, A34, A35, Th67;
(f . p1) `2 <= (f . p2) `2 by A2, A20, A30, A33, Th71;
then A58: LE f . p1,f . p2,P by A5, A22, A25, A32, A54, A55, JGRAPH_5:51;
(f . p2) `2 <= (f . p3) `2 by A2, A30, A34, A37, Th71;
then A59: LE f . p2,f . p3,P by A5, A32, A36, A54, A56, A57, JGRAPH_5:51;

A60: now :: thesis:

per cases ;

case A61: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 ) ; :: thesis:

now :: thesis:

per cases by A50;

case ( p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p4 `2 ) ; :: thesis:

hence contradiction by A61, EUCLID:52; :: thesis:

end;

case p4 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis:

hence contradiction by A61, Th3; :: thesis:

end;

case p4 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis:

hence contradiction by A61, Th1; :: thesis:

end;

case A62: ( p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p4 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ; :: thesis:

then A63: p4 `2 = - 1 by Th3;
A64: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;
then A65: (W-min (rectangle ((- 1),1,(- 1),1))) `1 = - 1 by EUCLID:52;
(W-min (rectangle ((- 1),1,(- 1),1))) `2 = - 1 by A64, EUCLID:52;
hence contradiction by A61, A62, A63, A65, TOPREAL3:6; :: thesis:

end;

hence contradiction ; :: thesis:

end;

case A66: ( not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) ; :: thesis:

A67: ( p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) or p4 in LSeg (|[(- 1),1]|,|[1,1]|) or p4 in LSeg (|[1,1]|,|[1,(- 1)]|) or p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ) by A12, Th63;

now :: thesis:

per cases by A66;

case A68: p4 `1 <> - 1 ; :: thesis:

A69: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A70: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A71: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A72: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A5, JGRAPH_5:34;
A73: f . p1 in P by A9, A69, A70, FUNCT_1:def 6;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A5, JGRAPH_5:35;
then A74: f . p1 in Lower_Arc P by A71, A73;
A75: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A76: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A70, A75, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

now :: thesis:

per cases by A67, A68, Th1;

case p4 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis:

then A77: p4 `2 = 1 by Th3;
A78: f . p4 in P by A12, A69, A70, FUNCT_1:def 6;
(f . p4) `2 >= 0 by A2, A77, Th69;
then f . p4 in Upper_Arc P by A72, A78;
hence LE f . p4,f . p1,P by A74, A76, JORDAN6:def 10; :: thesis:

end;

case p4 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis:

then A79: p4 `1 = 1 by Th1;
A80: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A81: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A82: f . p4 in P by A12, A80, FUNCT_1:def 6;
A83: f . p1 in P by A9, A80, A81, FUNCT_1:def 6;
A84: (f . p1) `1 < 0 by A2, A21, A29, Th67;
A85: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A86: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A87: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A81, A86, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

A88: (f . p4) `1 >= 0 by A2, A79, Th68;

now :: thesis:

per cases ) `2 >= 0 or (f . p4) `2 < 0 ) ;

case A89: (f . p4) `2 >= 0 ; :: thesis:

A90: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A91: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A5, JGRAPH_5:34;
A92: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A93: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A81, A92, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

A94: f . p4 in Upper_Arc P by A82, A89, A91;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A5, JGRAPH_5:35;
then f . p1 in Lower_Arc P by A83, A90;
hence LE f . p4,f . p1,P by A93, A94, JORDAN6:def 10; :: thesis:

end;

case (f . p4) `2 < 0 ; :: thesis:

hence LE f . p4,f . p1,P by A5, A82, A83, A84, A85, A87, A88, JGRAPH_5:56; :: thesis:

end;

hence LE f . p4,f . p1,P ; :: thesis:

end;

case A95: p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis:

then p4 `2 = - 1 by Th3;
then A96: (f . p4) `2 < 0 by A2, Th69;
A97: f . p4 in P by A12, A69, A70, FUNCT_1:def 6;
A98: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
(f . p4) `1 >= (f . p1) `1 by A2, A20, A95, Th70;
hence LE f . p4,f . p1,P by A5, A73, A76, A96, A97, A98, JGRAPH_5:56; :: thesis:

end;

hence LE f . p4,f . p1,P ; :: thesis:

end;

case A99: ( p4 `1 = - 1 & p4 `2 >= 0 ) ; :: thesis:

A100: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A101: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A102: f . p4 in P by A12, A100, FUNCT_1:def 6;
A103: f . p1 in P by A9, A100, A101, FUNCT_1:def 6;
A104: (f . p4) `2 >= 0 by A2, A99, Th69;
A105: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A106: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A5, JGRAPH_5:34;
A107: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A108: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A101, A107, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

A109: f . p4 in Upper_Arc P by A102, A104, A106;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A5, JGRAPH_5:35;
then f . p1 in Lower_Arc P by A103, A105;
hence LE f . p4,f . p1,P by A108, A109, JORDAN6:def 10; :: thesis:

end;

case A110: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 ) ; :: thesis:

then A111: p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by A13, Th2;
A112: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A113: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A114: f . p4 in P by A12, A112, FUNCT_1:def 6;
A115: f . p1 in P by A9, A112, A113, FUNCT_1:def 6;
A116: (f . p1) `1 < 0 by A2, A21, A29, Th67;
A117: (f . p1) `2 < 0 by A2, A21, A29, Th67;
A118: (f . p4) `2 <= (f . p1) `2 by A2, A20, A29, A110, A111, Th71;
(f . p4) `1 < 0 by A2, A110, Th68;
hence LE f . p4,f . p1,P by A5, A114, A115, A116, A117, A118, JGRAPH_5:51; :: thesis:

end;

hence LE f . p4,f . p1,P ; :: thesis:

end;

A119: rectangle ((- 1),1,(- 1),1) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } by Lm15;
thus rectangle ((- 1),1,(- 1),1) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( - 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) or ( 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) ) } :: thesis:

proof

thus rectangle ((- 1),1,(- 1),1) c= { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( - 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) or ( 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) ) } :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rectangle ((- 1),1,(- 1),1) ; :: thesis:
then ex p being Point of (TOP-REAL 2) st
( p = x & ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) ) by A119;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( - 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) or ( 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) ) } ; :: thesis:

end;

thus { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( - 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) or ( 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) ) } c= rectangle ((- 1),1,(- 1),1) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( - 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) or ( 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) ) } ; :: thesis:
then ex p being Point of (TOP-REAL 2) st
( p = x & ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( - 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) or ( 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) ) ) ;
hence x in rectangle ((- 1),1,(- 1),1) by A119; :: thesis:

end;

thus f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A58, A59, A60, JORDAN17:def 1; :: thesis:

end;

hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis:

end;

case A120: ( not p3 `2 < 0 or not p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis:

A121: now :: thesis:

per cases by A11, Th63;

case p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ; :: thesis:

hence ( ( p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p3 `2 ) or p3 in LSeg (|[(- 1),1]|,|[1,1]|) or p3 in LSeg (|[1,1]|,|[1,(- 1)]|) or ( p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p3 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ) by A120, EUCLID:52; :: thesis:

end;

case p3 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis:

end;

case p3 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis:

end;

case A122: p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis:

A123: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;

now :: thesis:

assume A124: p3 = W-min (rectangle ((- 1),1,(- 1),1)) ; :: thesis:
then p3 `2 = - 1 by A123, EUCLID:52;
hence contradiction by A120, A123, A124, RLTOPSP1:68; :: thesis:

end;

then A125: LE |[(- 1),0]|,p3, rectangle ((- 1),1,(- 1),1) by A19, Th59;
A126: (f . p2) `1 < 0 by A2, A30, A31, Th67;
A127: (f . p2) `2 < 0 by A2, A30, A31, Th67;
(f . p1) `2 <= (f . p2) `2 by A2, A20, A30, A33, Th71;
then A128: LE f . p1,f . p2,P by A5, A22, A25, A32, A126, A127, JGRAPH_5:51;
A129: LE f . p3,f . p4,P by A1, A2, A8, A17, A18, A125, Th66, RLTOPSP1:69;

A130: now :: thesis:

per cases ;

case A131: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 ) ; :: thesis:

A132: |[(- 1),(- 1)]| `1 = - 1 by EUCLID:52;
A133: |[(- 1),(- 1)]| `2 = - 1 by EUCLID:52;
A134: |[(- 1),1]| `1 = - 1 by EUCLID:52;
A135: |[(- 1),1]| `2 = 1 by EUCLID:52;
- 1 <= p4 `2 by A12, Th19;
then A136: p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by A131, A132, A133, A134, A135, GOBOARD7:7;

now :: thesis:

per cases by A121;

case A137: ( p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p3 `2 ) ; :: thesis:

then 0 <= p3 `2 by EUCLID:52;
hence contradiction by A8, A131, A136, A137, Th55; :: thesis:

end;

case A138: p3 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis:

then LE p4,p3, rectangle ((- 1),1,(- 1),1) by A136, Th59;
then p3 = p4 by A8, Th50, JORDAN6:57;
hence contradiction by A131, A138, Th3; :: thesis:

end;

case A139: p3 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis:

then LE p4,p3, rectangle ((- 1),1,(- 1),1) by A136, Th59;
then p3 = p4 by A8, Th50, JORDAN6:57;
hence contradiction by A131, A139, Th1; :: thesis:

end;

case A140: ( p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p3 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ; :: thesis:

then LE p4,p3, rectangle ((- 1),1,(- 1),1) by A136, Th59;
then A141: p3 = p4 by A8, Th50, JORDAN6:57;
A142: p3 `2 = - 1 by A140, Th3;
A143: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;
then A144: (W-min (rectangle ((- 1),1,(- 1),1))) `1 = - 1 by EUCLID:52;
(W-min (rectangle ((- 1),1,(- 1),1))) `2 = - 1 by A143, EUCLID:52;
hence contradiction by A131, A140, A141, A142, A144, TOPREAL3:6; :: thesis:

end;

hence contradiction ; :: thesis:

end;

case A145: ( not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) ; :: thesis:

A146: ( p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) or p4 in LSeg (|[(- 1),1]|,|[1,1]|) or p4 in LSeg (|[1,1]|,|[1,(- 1)]|) or p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ) by A12, Th63;

now :: thesis:

per cases by A145;

case A147: p4 `1 <> - 1 ; :: thesis:

A148: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A149: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A150: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A151: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A5, JGRAPH_5:34;
A152: f . p1 in P by A9, A148, A149, FUNCT_1:def 6;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A5, JGRAPH_5:35;
then A153: f . p1 in Lower_Arc P by A150, A152;
A154: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A155: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A149, A154, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

now :: thesis:

per cases by A146, A147, Th1;

case p4 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis:

then A156: p4 `2 = 1 by Th3;
A157: f . p4 in P by A12, A148, A149, FUNCT_1:def 6;
(f . p4) `2 >= 0 by A2, A156, Th69;
then f . p4 in Upper_Arc P by A151, A157;
hence LE f . p4,f . p1,P by A153, A155, JORDAN6:def 10; :: thesis:

end;

case p4 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis:

then A158: p4 `1 = 1 by Th1;
A159: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A160: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A161: f . p4 in P by A12, A159, FUNCT_1:def 6;
A162: f . p1 in P by A9, A159, A160, FUNCT_1:def 6;
A163: (f . p1) `1 < 0 by A2, A21, A29, Th67;
A164: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A165: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A166: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A160, A165, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

A167: (f . p4) `1 >= 0 by A2, A158, Th68;

now :: thesis:

per cases ) `2 >= 0 or (f . p4) `2 < 0 ) ;

case A168: (f . p4) `2 >= 0 ; :: thesis:

A169: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A170: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A5, JGRAPH_5:34;
A171: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A172: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A160, A171, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

A173: f . p4 in Upper_Arc P by A161, A168, A170;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A5, JGRAPH_5:35;
then f . p1 in Lower_Arc P by A162, A169;
hence LE f . p4,f . p1,P by A172, A173, JORDAN6:def 10; :: thesis:

end;

case (f . p4) `2 < 0 ; :: thesis:

hence LE f . p4,f . p1,P by A5, A161, A162, A163, A164, A166, A167, JGRAPH_5:56; :: thesis:

end;

hence LE f . p4,f . p1,P ; :: thesis:

end;

case A174: p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis:

then p4 `2 = - 1 by Th3;
then A175: (f . p4) `2 < 0 by A2, Th69;
A176: f . p4 in P by A12, A148, A149, FUNCT_1:def 6;
A177: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
(f . p4) `1 >= (f . p1) `1 by A2, A20, A174, Th70;
hence LE f . p4,f . p1,P by A5, A152, A155, A175, A176, A177, JGRAPH_5:56; :: thesis:

end;

hence LE f . p4,f . p1,P ; :: thesis:

end;

case A178: ( p4 `1 = - 1 & p4 `2 >= 0 ) ; :: thesis:

A179: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A180: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A181: f . p4 in P by A12, A179, FUNCT_1:def 6;
A182: f . p1 in P by A9, A179, A180, FUNCT_1:def 6;
A183: (f . p4) `2 >= 0 by A2, A178, Th69;
A184: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A185: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A5, JGRAPH_5:34;
A186: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A187: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A180, A186, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

A188: f . p4 in Upper_Arc P by A181, A183, A185;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A5, JGRAPH_5:35;
then f . p1 in Lower_Arc P by A182, A184;
hence LE f . p4,f . p1,P by A187, A188, JORDAN6:def 10; :: thesis:

end;

case A189: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 ) ; :: thesis:

then A190: p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by A13, Th2;
A191: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A192: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A193: f . p4 in P by A12, A191, FUNCT_1:def 6;
A194: f . p1 in P by A9, A191, A192, FUNCT_1:def 6;
A195: (f . p1) `1 < 0 by A2, A21, A29, Th67;
A196: (f . p1) `2 < 0 by A2, A21, A29, Th67;
A197: (f . p4) `2 <= (f . p1) `2 by A2, A20, A29, A189, A190, Th71;
(f . p4) `1 < 0 by A2, A189, Th68;
hence LE f . p4,f . p1,P by A5, A193, A194, A195, A196, A197, JGRAPH_5:51; :: thesis:

end;

hence LE f . p4,f . p1,P ; :: thesis:

end;

A198: rectangle ((- 1),1,(- 1),1) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } by Lm15;
thus rectangle ((- 1),1,(- 1),1) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( - 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) or ( 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) ) } :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rectangle ((- 1),1,(- 1),1) ; :: thesis:
then ex p being Point of (TOP-REAL 2) st
( p = x & ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) ) by A198;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( - 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) or ( 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) ) } ; :: thesis:

end;

proof

end;

thus f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A128, A129, A130, JORDAN17:def 1; :: thesis:

end;

hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis:

end;

case A199: ( not p2 `2 < 0 or not p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis:

A200: now :: thesis:

per cases by A10, Th63;

case p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ; :: thesis:

hence ( ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p2 `2 ) or p2 in LSeg (|[(- 1),1]|,|[1,1]|) or p2 in LSeg (|[1,1]|,|[1,(- 1)]|) or ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ) by A199, EUCLID:52; :: thesis:

end;

case p2 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis:

end;

case p2 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis:

end;

case A201: p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis:

A202: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;

now :: thesis:

assume A203: p2 = W-min (rectangle ((- 1),1,(- 1),1)) ; :: thesis:
then p2 `2 = - 1 by A202, EUCLID:52;
hence contradiction by A199, A202, A203, RLTOPSP1:68; :: thesis:

end;

then A204: LE |[(- 1),0]|,p2, rectangle ((- 1),1,(- 1),1) by A19, Th59;
then A205: LE f . p2,f . p3,P by A1, A2, A7, A17, A18, Th66, RLTOPSP1:69;
LE |[(- 1),0]|,p3, rectangle ((- 1),1,(- 1),1) by A7, A204, Th50, JORDAN6:58;
then A206: LE f . p3,f . p4,P by A1, A2, A8, A17, A18, Th66, RLTOPSP1:69;

A207: now :: thesis:

per cases ;

case A208: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 ) ; :: thesis:

A209: |[(- 1),(- 1)]| `1 = - 1 by EUCLID:52;
A210: |[(- 1),(- 1)]| `2 = - 1 by EUCLID:52;
A211: |[(- 1),1]| `1 = - 1 by EUCLID:52;
A212: |[(- 1),1]| `2 = 1 by EUCLID:52;
- 1 <= p4 `2 by A12, Th19;
then A213: p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by A208, A209, A210, A211, A212, GOBOARD7:7;

now :: thesis:

per cases by A200;

case A214: ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p2 `2 ) ; :: thesis:

then 0 <= p2 `2 by EUCLID:52;
hence contradiction by A15, A208, A213, A214, Th55; :: thesis:

end;

case A215: p2 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis:

then LE p4,p2, rectangle ((- 1),1,(- 1),1) by A213, Th59;
then p2 = p4 by A15, Th50, JORDAN6:57;
hence contradiction by A208, A215, Th3; :: thesis:

end;

case A216: p2 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis:

then LE p4,p2, rectangle ((- 1),1,(- 1),1) by A213, Th59;
then p2 = p4 by A15, Th50, JORDAN6:57;
hence contradiction by A208, A216, Th1; :: thesis:

end;

case A217: ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ; :: thesis:

then LE p4,p2, rectangle ((- 1),1,(- 1),1) by A213, Th59;
then A218: p2 = p4 by A15, Th50, JORDAN6:57;
A219: p2 `2 = - 1 by A217, Th3;
A220: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;
then A221: (W-min (rectangle ((- 1),1,(- 1),1))) `1 = - 1 by EUCLID:52;
(W-min (rectangle ((- 1),1,(- 1),1))) `2 = - 1 by A220, EUCLID:52;
hence contradiction by A208, A217, A218, A219, A221, TOPREAL3:6; :: thesis:

end;

hence contradiction ; :: thesis:

end;

case A222: ( not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) ; :: thesis:

A223: ( p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) or p4 in LSeg (|[(- 1),1]|,|[1,1]|) or p4 in LSeg (|[1,1]|,|[1,(- 1)]|) or p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ) by A12, Th63;

now :: thesis:

per cases by A222;

case A224: p4 `1 <> - 1 ; :: thesis:

A225: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A226: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A227: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A228: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A5, JGRAPH_5:34;
A229: f . p1 in P by A9, A225, A226, FUNCT_1:def 6;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A5, JGRAPH_5:35;
then A230: f . p1 in Lower_Arc P by A227, A229;
A231: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A232: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A226, A231, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

now :: thesis:

per cases by A223, A224, Th1;

case p4 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis:

then A233: p4 `2 = 1 by Th3;
A234: f . p4 in P by A12, A225, A226, FUNCT_1:def 6;
(f . p4) `2 >= 0 by A2, A233, Th69;
then f . p4 in Upper_Arc P by A228, A234;
hence LE f . p4,f . p1,P by A230, A232, JORDAN6:def 10; :: thesis:

end;

case p4 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis:

then A235: p4 `1 = 1 by Th1;
A236: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A237: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A238: f . p4 in P by A12, A236, FUNCT_1:def 6;
A239: f . p1 in P by A9, A236, A237, FUNCT_1:def 6;
A240: (f . p1) `1 < 0 by A2, A21, A29, Th67;
A241: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A242: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A243: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A237, A242, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

A244: (f . p4) `1 >= 0 by A2, A235, Th68;

now :: thesis:

per cases ) `2 >= 0 or (f . p4) `2 < 0 ) ;

case A245: (f . p4) `2 >= 0 ; :: thesis:

A246: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A247: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A5, JGRAPH_5:34;
A248: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A249: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A237, A248, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

A250: f . p4 in Upper_Arc P by A238, A245, A247;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A5, JGRAPH_5:35;
then f . p1 in Lower_Arc P by A239, A246;
hence LE f . p4,f . p1,P by A249, A250, JORDAN6:def 10; :: thesis:

end;

case (f . p4) `2 < 0 ; :: thesis:

hence LE f . p4,f . p1,P by A5, A238, A239, A240, A241, A243, A244, JGRAPH_5:56; :: thesis:

end;

hence LE f . p4,f . p1,P ; :: thesis:

end;

case A251: p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis:

then p4 `2 = - 1 by Th3;
then A252: (f . p4) `2 < 0 by A2, Th69;
A253: f . p4 in P by A12, A225, A226, FUNCT_1:def 6;
A254: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
(f . p4) `1 >= (f . p1) `1 by A2, A20, A251, Th70;
hence LE f . p4,f . p1,P by A5, A229, A232, A252, A253, A254, JGRAPH_5:56; :: thesis:

end;

hence LE f . p4,f . p1,P ; :: thesis:

end;

case A255: ( p4 `1 = - 1 & p4 `2 >= 0 ) ; :: thesis:

A256: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A257: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A258: f . p4 in P by A12, A256, FUNCT_1:def 6;
A259: f . p1 in P by A9, A256, A257, FUNCT_1:def 6;
A260: (f . p4) `2 >= 0 by A2, A255, Th69;
A261: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A262: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A5, JGRAPH_5:34;
A263: f . |[(- 1),0]| = W-min P by A2, A5, Th10, JGRAPH_5:29;

A264: now :: thesis:

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0]| by A2, A257, A263, FUNCT_1:def 4;
hence contradiction by A29, EUCLID:52; :: thesis:

end;

A265: f . p4 in Upper_Arc P by A258, A260, A262;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A5, JGRAPH_5:35;
then f . p1 in Lower_Arc P by A259, A261;
hence LE f . p4,f . p1,P by A264, A265, JORDAN6:def 10; :: thesis:

end;

case A266: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 ) ; :: thesis:

then A267: p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by A13, Th2;
A268: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A5, Lm15, Th35, JGRAPH_3:23;
A269: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A270: f . p4 in P by A12, A268, FUNCT_1:def 6;
A271: f . p1 in P by A9, A268, A269, FUNCT_1:def 6;
A272: (f . p1) `1 < 0 by A2, A21, A29, Th67;
A273: (f . p1) `2 < 0 by A2, A21, A29, Th67;
A274: (f . p4) `2 <= (f . p1) `2 by A2, A20, A29, A266, A267, Th71;
(f . p4) `1 < 0 by A2, A266, Th68;
hence LE f . p4,f . p1,P by A5, A270, A271, A272, A273, A274, JGRAPH_5:51; :: thesis:

end;

hence LE f . p4,f . p1,P ; :: thesis:

end;

A275: rectangle ((- 1),1,(- 1),1) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } by Lm15;
thus rectangle ((- 1),1,(- 1),1) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( - 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) or ( 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) ) } :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rectangle ((- 1),1,(- 1),1) ; :: thesis:
then ex p being Point of (TOP-REAL 2) st
( p = x & ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) ) by A275;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( - 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) or ( 1 = p `2 & - 1 <= p `1 & p `1 <= 1 ) ) } ; :: thesis:

end;

proof

end;

thus f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A205, A206, A207, JORDAN17:def 1; :: thesis:

end;

hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis:

end;

hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis:

end;

case A276: p1 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis:

A277: |[(- 1),1]| in LSeg (|[(- 1),1]|,|[1,1]|) by RLTOPSP1:68;
A278: |[(- 1),1]| `1 = - 1 by EUCLID:52;
A279: |[(- 1),1]| `2 = 1 by EUCLID:52;
- 1 <= p1 `1 by A276, Th3;
then A280: LE |[(- 1),1]|,p1, rectangle ((- 1),1,(- 1),1) by A276, A277, A278, Th60;
then A281: LE f . p1,f . p2,P by A1, A2, A6, A279, Th66, RLTOPSP1:68;
A282: LE |[(- 1),1]|,p2, rectangle ((- 1),1,(- 1),1) by A6, A280, Th50, JORDAN6:58;
then A283: LE f . p2,f . p3,P by A1, A2, A7, A279, Th66, RLTOPSP1:68;
LE |[(- 1),1]|,p3, rectangle ((- 1),1,(- 1),1) by A7, A282, Th50, JORDAN6:58;
then LE f . p3,f . p4,P by A1, A2, A8, A279, Th66, RLTOPSP1:68;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A281, A283, JORDAN17:def 1; :: thesis:

end;

case A284: p1 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis:

A285: |[(- 1),1]| in LSeg (|[(- 1),1]|,|[1,1]|) by RLTOPSP1:68;
A286: |[(- 1),1]| `1 = - 1 by EUCLID:52;
A287: |[(- 1),1]| `2 = 1 by EUCLID:52;
A288: |[1,1]| in LSeg (|[1,1]|,|[1,(- 1)]|) by RLTOPSP1:68;
A289: |[1,1]| in LSeg (|[(- 1),1]|,|[1,1]|) by RLTOPSP1:68;
A290: |[1,1]| `1 = 1 by EUCLID:52;
A291: |[1,1]| `2 = 1 by EUCLID:52;
A292: LE |[(- 1),1]|,|[1,1]|, rectangle ((- 1),1,(- 1),1) by A285, A286, A289, A290, Th60;
p1 `2 <= 1 by A284, Th1;
then LE |[1,1]|,p1, rectangle ((- 1),1,(- 1),1) by A284, A288, A291, Th61;
then A293: LE |[(- 1),1]|,p1, rectangle ((- 1),1,(- 1),1) by A292, Th50, JORDAN6:58;
then A294: LE f . p1,f . p2,P by A1, A2, A6, A287, Th66, RLTOPSP1:68;
A295: LE |[(- 1),1]|,p2, rectangle ((- 1),1,(- 1),1) by A6, A293, Th50, JORDAN6:58;
then A296: LE f . p2,f . p3,P by A1, A2, A7, A287, Th66, RLTOPSP1:68;
LE |[(- 1),1]|,p3, rectangle ((- 1),1,(- 1),1) by A7, A295, Th50, JORDAN6:58;
then LE f . p3,f . p4,P by A1, A2, A8, A287, Th66, RLTOPSP1:68;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A294, A296, JORDAN17:def 1; :: thesis:

end;

case A297: ( p1 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p1 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ; :: thesis:

A298: |[(- 1),1]| in LSeg (|[(- 1),1]|,|[1,1]|) by RLTOPSP1:68;
A299: |[(- 1),1]| `1 = - 1 by EUCLID:52;
A300: |[(- 1),1]| `2 = 1 by EUCLID:52;
A301: |[1,1]| in LSeg (|[(- 1),1]|,|[1,1]|) by RLTOPSP1:68;
|[1,1]| `1 = 1 by EUCLID:52;
then A302: LE |[(- 1),1]|,|[1,1]|, rectangle ((- 1),1,(- 1),1) by A298, A299, A301, Th60;
A303: |[1,(- 1)]| in LSeg (|[1,1]|,|[1,(- 1)]|) by RLTOPSP1:68;
A304: |[1,(- 1)]| in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) by RLTOPSP1:68;
A305: |[1,(- 1)]| `1 = 1 by EUCLID:52;
LE |[1,1]|,|[1,(- 1)]|, rectangle ((- 1),1,(- 1),1) by A301, A303, Th60;
then A306: LE |[(- 1),1]|,|[1,(- 1)]|, rectangle ((- 1),1,(- 1),1) by A302, Th50, JORDAN6:58;
W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;
then A307: (W-min (rectangle ((- 1),1,(- 1),1))) `1 = - 1 by EUCLID:52;
p1 `1 <= 1 by A297, Th3;
then LE |[1,(- 1)]|,p1, rectangle ((- 1),1,(- 1),1) by A297, A304, A305, A307, Th62;
then A308: LE |[(- 1),1]|,p1, rectangle ((- 1),1,(- 1),1) by A306, Th50, JORDAN6:58;
then A309: LE f . p1,f . p2,P by A1, A2, A6, A300, Th66, RLTOPSP1:68;
A310: LE |[(- 1),1]|,p2, rectangle ((- 1),1,(- 1),1) by A6, A308, Th50, JORDAN6:58;
then A311: LE f . p2,f . p3,P by A1, A2, A7, A300, Th66, RLTOPSP1:68;
LE |[(- 1),1]|,p3, rectangle ((- 1),1,(- 1),1) by A7, A310, Th50, JORDAN6:58;
then LE f . p3,f . p4,P by A1, A2, A8, A300, Th66, RLTOPSP1:68;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A309, A311, JORDAN17:def 1; :: thesis:

end;

hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis:

end;