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 A1: ( P = circle 0 ,0 ,1 & f = Sq_Circ ) ; :: thesis:
A2: rectangle (- 1),1,(- 1),1 is being_simple_closed_curve by Th60;
A3: 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 Lm8;
A4: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } by A1, Th33;
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:

proof

assume A5: ( LE p1,p2, rectangle (- 1),1,(- 1),1 & LE p2,p3, rectangle (- 1),1,(- 1),1 & LE p3,p4, rectangle (- 1),1,(- 1),1 ) ; :: thesis:
then A6: ( p1 in rectangle (- 1),1,(- 1),1 & p2 in rectangle (- 1),1,(- 1),1 ) by A2, JORDAN7:5;
A7: ( p3 in rectangle (- 1),1,(- 1),1 & p4 in rectangle (- 1),1,(- 1),1 ) by A2, A5, JORDAN7:5;
then consider q8 being Point of (TOP-REAL 2) such that
A8: ( 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 A3;
A9: LE p1,p3, rectangle (- 1),1,(- 1),1 by A5, Th60, JORDAN6:73;
A10: LE p2,p4, rectangle (- 1),1,(- 1),1 by A5, Th60, JORDAN6:73;
A11: W-min (rectangle (- 1),1,(- 1),1) = |[(- 1),(- 1)]| by Th56;
A12: ( |[(- 1),0 ]| `1 = - 1 & |[(- 1),0 ]| `2 = 0 ) by EUCLID:56;
A13: (1 / 2) * (|[(- 1),(- 1)]| + |[(- 1),1]|) = ((1 / 2) * |[(- 1),(- 1)]|) + ((1 / 2) * |[(- 1),1]|) by EUCLID:36
.= |[((1 / 2) * (- 1)),((1 / 2) * (- 1))]| + ((1 / 2) * |[(- 1),1]|) by EUCLID:62
.= |[((1 / 2) * (- 1)),((1 / 2) * (- 1))]| + |[((1 / 2) * (- 1)),((1 / 2) * 1)]| by EUCLID:62
.= |[(((1 / 2) * (- 1)) + ((1 / 2) * (- 1))),(((1 / 2) * (- 1)) + ((1 / 2) * 1))]| by EUCLID:60
.= |[(- 1),0 ]| ;
then A14: |[(- 1),0 ]| in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| by RLTOPSP1:70;

now

per cases by A6, A11, Th73, RLTOPSP1:69;

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

then A16: ( p1 `1 = - 1 & - 1 <= p1 `2 & p1 `2 <= 1 ) by Th9;
then A17: (f . p1) `1 < 0 by A1, Th78;
A18: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A19: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A20: f . p1 in P by A6, A18, FUNCT_1:def 12;

now

per cases ;

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

then A22: LE f . p1,f . p2,P by A1, A5, A15, Th75;
A23: LE f . p2,f . p3,P by A1, A5, A15, A21, Th76;
LE f . p3,f . p4,P by A1, A5, A9, A15, A21, Th76;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A22, A23, JORDAN17:def 1; :: thesis:

end;

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

now

per cases ;

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

then A26: ( p2 `1 = - 1 & - 1 <= p2 `2 & p2 `2 <= 1 ) by Th9;
A27: f . p2 in P by A6, A18, A19, FUNCT_1:def 12;
A28: p1 `2 <= p2 `2 by A5, A15, A25, Th65;

now

per cases ;

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

then A30: ( p3 `1 = - 1 & - 1 <= p3 `2 & p3 `2 <= 1 ) by Th9;
A31: f . p3 in P by A7, A18, A19, FUNCT_1:def 12;
A32: p2 `2 <= p3 `2 by A5, A25, A29, Th65;

now

per cases ;

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

then A34: ( p4 `1 = - 1 & - 1 <= p4 `2 & p4 `2 <= 1 ) by Th9;
A35: ( (f . p2) `1 < 0 & (f . p2) `2 < 0 ) by A1, A25, A26, Th77;
A36: ( (f . p3) `1 < 0 & (f . p3) `2 < 0 ) by A1, A29, A30, Th77;
A37: ( (f . p4) `1 < 0 & (f . p4) `2 < 0 ) by A1, A33, A34, Th77;
(f . p1) `2 <= (f . p2) `2 by A1, A15, A25, A28, Th81;
then A38: LE f . p1,f . p2,P by A4, A17, A20, A27, A35, JGRAPH_5:54;
(f . p2) `2 <= (f . p3) `2 by A1, A25, A29, A32, Th81;
then A39: LE f . p2,f . p3,P by A4, A27, A31, A35, A36, JGRAPH_5:54;
A40: f . p4 in P by A7, A18, A19, FUNCT_1:def 12;
p3 `2 <= p4 `2 by A5, A29, A33, Th65;
then (f . p3) `2 <= (f . p4) `2 by A1, A29, A33, Th81;
then LE f . p3,f . p4,P by A4, A31, A36, A37, A40, JGRAPH_5:54;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A38, A39, JORDAN17:def 1; :: thesis:

end;

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

A42: now

per cases by A7, Th73;

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 A41, EUCLID:56; :: thesis:

end;

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

end;

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

end;

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

A44: W-min (rectangle (- 1),1,(- 1),1) = |[(- 1),(- 1)]| by Th56;

now

assume A45: p4 = W-min (rectangle (- 1),1,(- 1),1) ; :: thesis:
then p4 `2 = - 1 by A44, EUCLID:56;
hence contradiction by A41, A44, A45, RLTOPSP1:69; :: thesis:

end;

A46: ( (f . p2) `1 < 0 & (f . p2) `2 < 0 ) by A1, A25, A26, Th77;
A47: ( (f . p3) `1 < 0 & (f . p3) `2 < 0 ) by A1, A29, A30, Th77;
(f . p1) `2 <= (f . p2) `2 by A1, A15, A25, A28, Th81;
then A48: LE f . p1,f . p2,P by A4, A17, A20, A27, A46, JGRAPH_5:54;
(f . p2) `2 <= (f . p3) `2 by A1, A25, A29, A32, Th81;
then A49: LE f . p2,f . p3,P by A4, A27, A31, A46, A47, JGRAPH_5:54;

A50: now

per cases ;

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

now

per cases by A42;

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

hence contradiction by A51, EUCLID:56; :: thesis:

end;

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

hence contradiction by A51, Th11; :: thesis:

end;

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

hence contradiction by A51, Th9; :: thesis:

end;

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

then A53: p4 `2 = - 1 by Th11;
W-min (rectangle (- 1),1,(- 1),1) = |[(- 1),(- 1)]| by Th56;
then ( (W-min (rectangle (- 1),1,(- 1),1)) `1 = - 1 & (W-min (rectangle (- 1),1,(- 1),1)) `2 = - 1 ) by EUCLID:56;
hence contradiction by A51, A52, A53, TOPREAL3:11; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

A55: ( 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 A7, Th73;

now

per cases by A54;

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

A57: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A58: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A59: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A60: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A4, JGRAPH_5:37;
A61: f . p1 in P by A6, A57, A58, FUNCT_1:def 12;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A4, JGRAPH_5:38;
then A62: f . p1 in Lower_Arc P by A59, A61;
A63: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A64: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A58, A63, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

now

per cases by A55, A56, Th9;

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

then A65: p4 `2 = 1 by Th11;
A66: f . p4 in P by A7, A57, A58, FUNCT_1:def 12;
(f . p4) `2 >= 0 by A1, A65, Th79;
then f . p4 in Upper_Arc P by A60, A66;
hence LE f . p4,f . p1,P by A62, A64, JORDAN6:def 10; :: thesis:

end;

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

then A67: p4 `1 = 1 by Th9;
A68: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A69: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A70: f . p4 in P by A7, A68, FUNCT_1:def 12;
A71: f . p1 in P by A6, A68, A69, FUNCT_1:def 12;
A72: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A73: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A74: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A69, A73, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

A75: (f . p4) `1 >= 0 by A1, A67, Th78;

now

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

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

A77: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A78: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A4, JGRAPH_5:37;
A79: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A80: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A69, A79, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

A81: f . p4 in Upper_Arc P by A70, A76, A78;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A4, JGRAPH_5:38;
then f . p1 in Lower_Arc P by A71, A77;
hence LE f . p4,f . p1,P by A80, A81, JORDAN6:def 10; :: thesis:

end;

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

hence LE f . p4,f . p1,P by A4, A70, A71, A72, A74, A75, JGRAPH_5:59; :: thesis:

end;

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

end;

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

then ( p4 `2 = - 1 & - 1 <= p4 `1 & p4 `1 <= 1 ) by Th11;
then A83: (f . p4) `2 < 0 by A1, Th79;
A84: f . p4 in P by A7, A57, A58, FUNCT_1:def 12;
A85: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
(f . p4) `1 >= (f . p1) `1 by A1, A15, A82, Th80;
hence LE f . p4,f . p1,P by A4, A61, A64, A83, A84, A85, JGRAPH_5:59; :: thesis:

end;

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

end;

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

A87: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A88: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A89: f . p4 in P by A7, A87, FUNCT_1:def 12;
A90: f . p1 in P by A6, A87, A88, FUNCT_1:def 12;
A91: (f . p4) `2 >= 0 by A1, A86, Th79;
A92: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A93: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A4, JGRAPH_5:37;
A94: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A95: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A88, A94, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

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

end;

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

then A98: p4 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| by A8, Th10;
A99: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A100: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A101: f . p4 in P by A7, A99, FUNCT_1:def 12;
A102: f . p1 in P by A6, A99, A100, FUNCT_1:def 12;
A103: ( (f . p1) `1 < 0 & (f . p1) `2 < 0 ) by A1, A16, A24, Th77;
A104: (f . p4) `2 <= (f . p1) `2 by A1, A15, A24, A97, A98, Th81;
(f . p4) `1 < 0 by A1, A97, Th78;
hence LE f . p4,f . p1,P by A4, A101, A102, A103, A104, JGRAPH_5:54; :: thesis:

end;

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

end;

A105: 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 Lm8;
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 set ; :: according to TARSKI:def 3 :: thesis:
assume x in rectangle (- 1),1,(- 1),1 ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A106: ( 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 A105;
thus 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 ) ) } by A106; :: 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 set ; :: 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 consider p being Point of (TOP-REAL 2) such that
A107: ( 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 ) ) ) ;
thus x in rectangle (- 1),1,(- 1),1 by A105, A107; :: thesis:

end;

thus f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A48, A49, A50, JORDAN17:def 1; :: thesis:

end;

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

end;

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

A109: now

per cases by A7, Th73;

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 A108, EUCLID:56; :: thesis:

end;

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

end;

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

end;

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

A111: W-min (rectangle (- 1),1,(- 1),1) = |[(- 1),(- 1)]| by Th56;

now

assume A112: p3 = W-min (rectangle (- 1),1,(- 1),1) ; :: thesis:
then p3 `2 = - 1 by A111, EUCLID:56;
hence contradiction by A108, A111, A112, RLTOPSP1:69; :: thesis:

end;

then A113: LE |[(- 1),0 ]|,p3, rectangle (- 1),1,(- 1),1 by A14, Th69;
A114: ( (f . p2) `1 < 0 & (f . p2) `2 < 0 ) by A1, A25, A26, Th77;
(f . p1) `2 <= (f . p2) `2 by A1, A15, A25, A28, Th81;
then A115: LE f . p1,f . p2,P by A4, A17, A20, A27, A114, JGRAPH_5:54;
A116: LE f . p3,f . p4,P by A1, A5, A12, A13, A113, Th76, RLTOPSP1:70;

A117: now

per cases ;

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

A119: |[(- 1),(- 1)]| `1 = - 1 by EUCLID:56;
A120: |[(- 1),(- 1)]| `2 = - 1 by EUCLID:56;
A121: |[(- 1),1]| `1 = - 1 by EUCLID:56;
A122: |[(- 1),1]| `2 = 1 by EUCLID:56;
( - 1 <= p4 `2 & p4 `2 <= 1 ) by A7, Th28;
then A123: p4 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| by A118, A119, A120, A121, A122, GOBOARD7:8;

now

per cases by A109;

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

then 0 <= p3 `2 by EUCLID:56;
hence contradiction by A5, A118, A123, A124, Th65; :: thesis:

end;

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

then LE p4,p3, rectangle (- 1),1,(- 1),1 by A123, Th69;
then p3 = p4 by A5, Th60, JORDAN6:72;
hence contradiction by A118, A125, Th11; :: thesis:

end;

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

then LE p4,p3, rectangle (- 1),1,(- 1),1 by A123, Th69;
then p3 = p4 by A5, Th60, JORDAN6:72;
hence contradiction by A118, A126, Th9; :: thesis:

end;

case A127: ( 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 A123, Th69;
then A128: p3 = p4 by A5, Th60, JORDAN6:72;
A129: p3 `2 = - 1 by A127, Th11;
W-min (rectangle (- 1),1,(- 1),1) = |[(- 1),(- 1)]| by Th56;
then ( (W-min (rectangle (- 1),1,(- 1),1)) `1 = - 1 & (W-min (rectangle (- 1),1,(- 1),1)) `2 = - 1 ) by EUCLID:56;
hence contradiction by A118, A127, A128, A129, TOPREAL3:11; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

A131: ( 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 A7, Th73;

now

per cases by A130;

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

A133: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A134: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A135: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A136: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A4, JGRAPH_5:37;
A137: f . p1 in P by A6, A133, A134, FUNCT_1:def 12;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A4, JGRAPH_5:38;
then A138: f . p1 in Lower_Arc P by A135, A137;
A139: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A140: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A134, A139, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

now

per cases by A131, A132, Th9;

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

then A141: p4 `2 = 1 by Th11;
A142: f . p4 in P by A7, A133, A134, FUNCT_1:def 12;
(f . p4) `2 >= 0 by A1, A141, Th79;
then f . p4 in Upper_Arc P by A136, A142;
hence LE f . p4,f . p1,P by A138, A140, JORDAN6:def 10; :: thesis:

end;

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

then A143: p4 `1 = 1 by Th9;
A144: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A145: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A146: f . p4 in P by A7, A144, FUNCT_1:def 12;
A147: f . p1 in P by A6, A144, A145, FUNCT_1:def 12;
A148: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A149: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A150: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A145, A149, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

A151: (f . p4) `1 >= 0 by A1, A143, Th78;

now

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

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

A153: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A154: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A4, JGRAPH_5:37;
A155: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A156: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A145, A155, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

A157: f . p4 in Upper_Arc P by A146, A152, A154;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A4, JGRAPH_5:38;
then f . p1 in Lower_Arc P by A147, A153;
hence LE f . p4,f . p1,P by A156, A157, JORDAN6:def 10; :: thesis:

end;

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

hence LE f . p4,f . p1,P by A4, A146, A147, A148, A150, A151, JGRAPH_5:59; :: thesis:

end;

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

end;

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

then ( p4 `2 = - 1 & - 1 <= p4 `1 & p4 `1 <= 1 ) by Th11;
then A159: (f . p4) `2 < 0 by A1, Th79;
A160: f . p4 in P by A7, A133, A134, FUNCT_1:def 12;
A161: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
(f . p4) `1 >= (f . p1) `1 by A1, A15, A158, Th80;
hence LE f . p4,f . p1,P by A4, A137, A140, A159, A160, A161, JGRAPH_5:59; :: thesis:

end;

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

end;

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

A163: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A164: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A165: f . p4 in P by A7, A163, FUNCT_1:def 12;
A166: f . p1 in P by A6, A163, A164, FUNCT_1:def 12;
A167: (f . p4) `2 >= 0 by A1, A162, Th79;
A168: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A169: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A4, JGRAPH_5:37;
A170: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A171: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A164, A170, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

A172: f . p4 in Upper_Arc P by A165, A167, A169;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A4, JGRAPH_5:38;
then f . p1 in Lower_Arc P by A166, A168;
hence LE f . p4,f . p1,P by A171, A172, JORDAN6:def 10; :: thesis:

end;

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

then A174: p4 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| by A8, Th10;
A175: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A176: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A177: f . p4 in P by A7, A175, FUNCT_1:def 12;
A178: f . p1 in P by A6, A175, A176, FUNCT_1:def 12;
A179: ( (f . p1) `1 < 0 & (f . p1) `2 < 0 ) by A1, A16, A24, Th77;
A180: (f . p4) `2 <= (f . p1) `2 by A1, A15, A24, A173, A174, Th81;
(f . p4) `1 < 0 by A1, A173, Th78;
hence LE f . p4,f . p1,P by A4, A177, A178, A179, A180, JGRAPH_5:54; :: thesis:

end;

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

end;

A181: 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 Lm8;
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 set ; :: according to TARSKI:def 3 :: thesis:
assume x in rectangle (- 1),1,(- 1),1 ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A182: ( 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 A181;
thus 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 ) ) } by A182; :: thesis:

end;

proof

let x be set ; :: 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 consider p being Point of (TOP-REAL 2) such that
A183: ( 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 ) ) ) ;
thus x in rectangle (- 1),1,(- 1),1 by A181, A183; :: thesis:

end;

thus f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A115, A116, A117, JORDAN17:def 1; :: thesis:

end;

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

end;

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

A185: now

per cases by A6, Th73;

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 A184, EUCLID:56; :: thesis:

end;

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

end;

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

end;

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

A187: W-min (rectangle (- 1),1,(- 1),1) = |[(- 1),(- 1)]| by Th56;

now

assume A188: p2 = W-min (rectangle (- 1),1,(- 1),1) ; :: thesis:
then p2 `2 = - 1 by A187, EUCLID:56;
hence contradiction by A184, A187, A188, RLTOPSP1:69; :: thesis:

end;

then A189: LE |[(- 1),0 ]|,p2, rectangle (- 1),1,(- 1),1 by A14, Th69;
then A190: LE f . p2,f . p3,P by A1, A5, A12, A13, Th76, RLTOPSP1:70;
LE |[(- 1),0 ]|,p3, rectangle (- 1),1,(- 1),1 by A5, A189, Th60, JORDAN6:73;
then A191: LE f . p3,f . p4,P by A1, A5, A12, A13, Th76, RLTOPSP1:70;

A192: now

per cases ;

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

A194: |[(- 1),(- 1)]| `1 = - 1 by EUCLID:56;
A195: |[(- 1),(- 1)]| `2 = - 1 by EUCLID:56;
A196: |[(- 1),1]| `1 = - 1 by EUCLID:56;
A197: |[(- 1),1]| `2 = 1 by EUCLID:56;
( - 1 <= p4 `2 & p4 `2 <= 1 ) by A7, Th28;
then A198: p4 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| by A193, A194, A195, A196, A197, GOBOARD7:8;

now

per cases by A185;

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

then 0 <= p2 `2 by EUCLID:56;
hence contradiction by A10, A193, A198, A199, Th65; :: thesis:

end;

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

then LE p4,p2, rectangle (- 1),1,(- 1),1 by A198, Th69;
then p2 = p4 by A10, Th60, JORDAN6:72;
hence contradiction by A193, A200, Th11; :: thesis:

end;

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

then LE p4,p2, rectangle (- 1),1,(- 1),1 by A198, Th69;
then p2 = p4 by A10, Th60, JORDAN6:72;
hence contradiction by A193, A201, Th9; :: thesis:

end;

case A202: ( 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 A198, Th69;
then A203: p2 = p4 by A10, Th60, JORDAN6:72;
A204: p2 `2 = - 1 by A202, Th11;
W-min (rectangle (- 1),1,(- 1),1) = |[(- 1),(- 1)]| by Th56;
then ( (W-min (rectangle (- 1),1,(- 1),1)) `1 = - 1 & (W-min (rectangle (- 1),1,(- 1),1)) `2 = - 1 ) by EUCLID:56;
hence contradiction by A193, A202, A203, A204, TOPREAL3:11; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

A206: ( 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 A7, Th73;

now

per cases by A205;

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

A208: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A209: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A210: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A211: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A4, JGRAPH_5:37;
A212: f . p1 in P by A6, A208, A209, FUNCT_1:def 12;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A4, JGRAPH_5:38;
then A213: f . p1 in Lower_Arc P by A210, A212;
A214: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A215: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A209, A214, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

now

per cases by A206, A207, Th9;

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

then A216: p4 `2 = 1 by Th11;
A217: f . p4 in P by A7, A208, A209, FUNCT_1:def 12;
(f . p4) `2 >= 0 by A1, A216, Th79;
then f . p4 in Upper_Arc P by A211, A217;
hence LE f . p4,f . p1,P by A213, A215, JORDAN6:def 10; :: thesis:

end;

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

then A218: p4 `1 = 1 by Th9;
A219: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A220: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A221: f . p4 in P by A7, A219, FUNCT_1:def 12;
A222: f . p1 in P by A6, A219, A220, FUNCT_1:def 12;
A223: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A224: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A225: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A220, A224, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

A226: (f . p4) `1 >= 0 by A1, A218, Th78;

now

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

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

A228: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A229: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A4, JGRAPH_5:37;
A230: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A231: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A220, A230, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

A232: f . p4 in Upper_Arc P by A221, A227, A229;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A4, JGRAPH_5:38;
then f . p1 in Lower_Arc P by A222, A228;
hence LE f . p4,f . p1,P by A231, A232, JORDAN6:def 10; :: thesis:

end;

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

hence LE f . p4,f . p1,P by A4, A221, A222, A223, A225, A226, JGRAPH_5:59; :: thesis:

end;

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

end;

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

then ( p4 `2 = - 1 & - 1 <= p4 `1 & p4 `1 <= 1 ) by Th11;
then A234: (f . p4) `2 < 0 by A1, Th79;
A235: f . p4 in P by A7, A208, A209, FUNCT_1:def 12;
A236: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
(f . p4) `1 >= (f . p1) `1 by A1, A15, A233, Th80;
hence LE f . p4,f . p1,P by A4, A212, A215, A234, A235, A236, JGRAPH_5:59; :: thesis:

end;

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

end;

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

A238: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A239: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A240: f . p4 in P by A7, A238, FUNCT_1:def 12;
A241: f . p1 in P by A6, A238, A239, FUNCT_1:def 12;
A242: (f . p4) `2 >= 0 by A1, A237, Th79;
A243: ( (f . p1) `1 < 0 & (f . p1) `2 <= 0 ) by A1, A16, A24, Th77;
A244: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A4, JGRAPH_5:37;
A245: f . |[(- 1),0 ]| = W-min P by A1, A4, Th18, JGRAPH_5:32;

A246: now

assume f . p1 = W-min P ; :: thesis:
then p1 = |[(- 1),0 ]| by A1, A239, A245, FUNCT_1:def 8;
hence contradiction by A24, EUCLID:56; :: thesis:

end;

A247: f . p4 in Upper_Arc P by A240, A242, A244;
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A4, JGRAPH_5:38;
then f . p1 in Lower_Arc P by A241, A243;
hence LE f . p4,f . p1,P by A246, A247, JORDAN6:def 10; :: thesis:

end;

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

then A249: p4 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| by A8, Th10;
A250: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A4, Lm8, Th45, JGRAPH_3:33;
A251: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A252: f . p4 in P by A7, A250, FUNCT_1:def 12;
A253: f . p1 in P by A6, A250, A251, FUNCT_1:def 12;
A254: ( (f . p1) `1 < 0 & (f . p1) `2 < 0 ) by A1, A16, A24, Th77;
A255: (f . p4) `2 <= (f . p1) `2 by A1, A15, A24, A248, A249, Th81;
(f . p4) `1 < 0 by A1, A248, Th78;
hence LE f . p4,f . p1,P by A4, A252, A253, A254, A255, JGRAPH_5:54; :: thesis:

end;

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

end;

A256: 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 Lm8;
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 set ; :: according to TARSKI:def 3 :: thesis:
assume x in rectangle (- 1),1,(- 1),1 ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A257: ( 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 A256;
thus 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 ) ) } by A257; :: thesis:

end;

proof

let x be set ; :: 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 consider p being Point of (TOP-REAL 2) such that
A258: ( 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 ) ) ) ;
thus x in rectangle (- 1),1,(- 1),1 by A256, A258; :: thesis:

end;

thus f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A190, A191, A192, 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 A259: p1 in LSeg |[(- 1),1]|,|[1,1]| ; :: thesis:

A260: |[(- 1),1]| in LSeg |[(- 1),1]|,|[1,1]| by RLTOPSP1:69;
A261: |[(- 1),1]| in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| by RLTOPSP1:69;
A262: ( |[(- 1),1]| `1 = - 1 & |[(- 1),1]| `2 = 1 ) by EUCLID:56;
( p1 `2 = 1 & - 1 <= p1 `1 & p1 `1 <= 1 ) by A259, Th11;
then A263: LE |[(- 1),1]|,p1, rectangle (- 1),1,(- 1),1 by A259, A260, A262, Th70;
then A264: LE f . p1,f . p2,P by A1, A5, A261, A262, Th76;
A265: LE |[(- 1),1]|,p2, rectangle (- 1),1,(- 1),1 by A5, A263, Th60, JORDAN6:73;
then A266: LE f . p2,f . p3,P by A1, A5, A261, A262, Th76;
LE |[(- 1),1]|,p3, rectangle (- 1),1,(- 1),1 by A5, A265, Th60, JORDAN6:73;
then LE f . p3,f . p4,P by A1, A5, A261, A262, Th76;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A264, A266, JORDAN17:def 1; :: thesis:

end;

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

A268: |[(- 1),1]| in LSeg |[(- 1),1]|,|[1,1]| by RLTOPSP1:69;
A269: |[(- 1),1]| in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| by RLTOPSP1:69;
A270: ( |[(- 1),1]| `1 = - 1 & |[(- 1),1]| `2 = 1 ) by EUCLID:56;
A271: |[1,1]| in LSeg |[1,1]|,|[1,(- 1)]| by RLTOPSP1:69;
A272: |[1,1]| in LSeg |[(- 1),1]|,|[1,1]| by RLTOPSP1:69;
A273: ( |[1,1]| `1 = 1 & |[1,1]| `2 = 1 ) by EUCLID:56;
then A274: LE |[(- 1),1]|,|[1,1]|, rectangle (- 1),1,(- 1),1 by A268, A270, A272, Th70;
( p1 `1 = 1 & - 1 <= p1 `2 & p1 `2 <= 1 ) by A267, Th9;
then LE |[1,1]|,p1, rectangle (- 1),1,(- 1),1 by A267, A271, A273, Th71;
then A275: LE |[(- 1),1]|,p1, rectangle (- 1),1,(- 1),1 by A274, Th60, JORDAN6:73;
then A276: LE f . p1,f . p2,P by A1, A5, A269, A270, Th76;
A277: LE |[(- 1),1]|,p2, rectangle (- 1),1,(- 1),1 by A5, A275, Th60, JORDAN6:73;
then A278: LE f . p2,f . p3,P by A1, A5, A269, A270, Th76;
LE |[(- 1),1]|,p3, rectangle (- 1),1,(- 1),1 by A5, A277, Th60, JORDAN6:73;
then LE f . p3,f . p4,P by A1, A5, A269, A270, Th76;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A276, A278, JORDAN17:def 1; :: thesis:

end;

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

A280: |[(- 1),1]| in LSeg |[(- 1),1]|,|[1,1]| by RLTOPSP1:69;
A281: |[(- 1),1]| in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| by RLTOPSP1:69;
A282: ( |[(- 1),1]| `1 = - 1 & |[(- 1),1]| `2 = 1 ) by EUCLID:56;
A283: |[1,1]| in LSeg |[(- 1),1]|,|[1,1]| by RLTOPSP1:69;
( |[1,1]| `1 = 1 & |[1,1]| `2 = 1 ) by EUCLID:56;
then A284: LE |[(- 1),1]|,|[1,1]|, rectangle (- 1),1,(- 1),1 by A280, A282, A283, Th70;
A285: |[1,(- 1)]| in LSeg |[1,1]|,|[1,(- 1)]| by RLTOPSP1:69;
A286: |[1,(- 1)]| in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| by RLTOPSP1:69;
A287: ( |[1,(- 1)]| `1 = 1 & |[1,(- 1)]| `2 = - 1 ) by EUCLID:56;
LE |[1,1]|,|[1,(- 1)]|, rectangle (- 1),1,(- 1),1 by A283, A285, Th70;
then A288: LE |[(- 1),1]|,|[1,(- 1)]|, rectangle (- 1),1,(- 1),1 by A284, Th60, JORDAN6:73;
W-min (rectangle (- 1),1,(- 1),1) = |[(- 1),(- 1)]| by Th56;
then A289: ( (W-min (rectangle (- 1),1,(- 1),1)) `1 = - 1 & (W-min (rectangle (- 1),1,(- 1),1)) `2 = - 1 ) by EUCLID:56;
( p1 `2 = - 1 & - 1 <= p1 `1 & p1 `1 <= 1 ) by A279, Th11;
then LE |[1,(- 1)]|,p1, rectangle (- 1),1,(- 1),1 by A279, A286, A287, A289, Th72;
then A290: LE |[(- 1),1]|,p1, rectangle (- 1),1,(- 1),1 by A288, Th60, JORDAN6:73;
then A291: LE f . p1,f . p2,P by A1, A5, A281, A282, Th76;
A292: LE |[(- 1),1]|,p2, rectangle (- 1),1,(- 1),1 by A5, A290, Th60, JORDAN6:73;
then A293: LE f . p2,f . p3,P by A1, A5, A281, A282, Th76;
LE |[(- 1),1]|,p3, rectangle (- 1),1,(- 1),1 by A5, A292, Th60, JORDAN6:73;
then LE f . p3,f . p4,P by A1, A5, A281, A282, Th76;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A291, A293, JORDAN17:def 1; :: thesis:

end;

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

end;