let p1, p2, p3, p4 be Point of (); :: thesis: for P being non empty compact Subset of ()
for f being Function of (),() st P = circle (0,0,1) & f = Sq_Circ & LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) holds
f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P

let P be non empty compact Subset of (); :: thesis: for f being Function of (),() st P = circle (0,0,1) & f = Sq_Circ & LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) holds
f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P

let f be Function of (),(); :: thesis: ( P = circle (0,0,1) & f = Sq_Circ & 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 )
set K = rectangle ((- 1),1,(- 1),1);
assume that
A1: P = circle (0,0,1) and
A2: f = Sq_Circ ; :: thesis: ( not LE p1,p2, rectangle ((- 1),1,(- 1),1) or not LE p2,p3, rectangle ((- 1),1,(- 1),1) or not LE p3,p4, rectangle ((- 1),1,(- 1),1) or f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P )
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 () : ( ( 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 () : |.p.| = 1 } by ;
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: verum
proof
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: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
A9: p1 in rectangle ((- 1),1,(- 1),1) by ;
A10: p2 in rectangle ((- 1),1,(- 1),1) by ;
A11: p3 in rectangle ((- 1),1,(- 1),1) by ;
A12: p4 in rectangle ((- 1),1,(- 1),1) by ;
then A13: ex q8 being Point of () 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 ;
A15: LE p2,p4, rectangle ((- 1),1,(- 1),1) by ;
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;
now :: thesis: ( ( p1 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) or ( p1 in LSeg (|[(- 1),1]|,|[1,1]|) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) or ( p1 in LSeg (|[1,1]|,|[1,(- 1)]|) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) or ( p1 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p1 <> W-min (rectangle ((- 1),1,(- 1),1)) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) )
per cases ( p1 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) or p1 in LSeg (|[(- 1),1]|,|[1,1]|) or p1 in LSeg (|[1,1]|,|[1,(- 1)]|) or ( p1 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p1 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ) by ;
case A20: p1 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
then A21: p1 `1 = - 1 by Th1;
then A22: (f . p1) `1 < 0 by ;
A23: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A24: dom f = the carrier of () by FUNCT_2:def 1;
then A25: f . p1 in P by ;
now :: thesis: ( ( p1 `2 >= 0 & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) or ( p1 `2 < 0 & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) )
per cases ( p1 `2 >= 0 or p1 `2 < 0 ) ;
case A26: p1 `2 >= 0 ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
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 ; :: thesis: verum
end;
case A29: p1 `2 < 0 ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
now :: thesis: ( ( p2 `2 < 0 & p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) or ( ( not p2 `2 < 0 or not p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) & rectangle ((- 1),1,(- 1),1) = { p where p is Point of () : ( ( 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 ) ) } & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) )
per cases ( ( p2 `2 < 0 & p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) or not p2 `2 < 0 or not p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ;
case A30: ( p2 `2 < 0 & p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
then A31: p2 `1 = - 1 by Th1;
A32: f . p2 in P by ;
A33: p1 `2 <= p2 `2 by A6, A20, A30, Th55;
now :: thesis: ( ( p3 `2 < 0 & p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) or ( ( not p3 `2 < 0 or not p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) & rectangle ((- 1),1,(- 1),1) = { p where p is Point of () : ( ( 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 ) ) } & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) )
per cases ( ( p3 `2 < 0 & p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) or not p3 `2 < 0 or not p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ;
case A34: ( p3 `2 < 0 & p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
then A35: p3 `1 = - 1 by Th1;
A36: f . p3 in P by ;
A37: p2 `2 <= p3 `2 by A7, A30, A34, Th55;
now :: thesis: ( ( p4 `2 < 0 & p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) or ( ( not p4 `2 < 0 or not p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) & rectangle ((- 1),1,(- 1),1) = { p where p is Point of () : ( ( 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 ) ) } & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) )
per cases ( ( p4 `2 < 0 & p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) or not p4 `2 < 0 or not p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ;
case A38: ( p4 `2 < 0 & p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
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 ;
(f . p2) `2 <= (f . p3) `2 by A2, A30, A34, A37, Th71;
then A47: LE f . p2,f . p3,P by ;
A48: f . p4 in P by ;
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 ;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by ; :: thesis: verum
end;
case A49: ( not p4 `2 < 0 or not p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis: ( rectangle ((- 1),1,(- 1),1) = { p where p is Point of () : ( ( 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 ) ) } & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P )
A50: now :: thesis: ( ( p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & ( ( 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)) ) ) ) or ( p4 in LSeg (|[(- 1),1]|,|[1,1]|) & ( ( 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)) ) ) ) or ( p4 in LSeg (|[1,1]|,|[1,(- 1)]|) & ( ( 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)) ) ) ) or ( p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & ( ( 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)) ) ) ) )
per cases ( 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 ;
case p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ; :: thesis: ( ( 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)) ) )
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 ; :: thesis: verum
end;
case p4 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: ( ( 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)) ) )
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)) ) ) ; :: thesis: verum
end;
case p4 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: ( ( 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)) ) )
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)) ) ) ; :: thesis: verum
end;
case A51: p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis: ( ( 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)) ) )
A52: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;
now :: thesis: not p4 = W-min (rectangle ((- 1),1,(- 1),1))
assume A53: p4 = W-min (rectangle ((- 1),1,(- 1),1)) ; :: thesis: contradiction
then p4 `2 = - 1 by ;
hence contradiction by A49, A52, A53, RLTOPSP1:68; :: thesis: verum
end;
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 A51; :: thesis: verum
end;
end;
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 ;
(f . p2) `2 <= (f . p3) `2 by A2, A30, A34, A37, Th71;
then A59: LE f . p2,f . p3,P by ;
A60: now :: thesis: ( ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 & contradiction ) or ( ( not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) & LE f . p4,f . p1,P ) )
per cases ( ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 ) or not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) ;
case A61: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 ) ; :: thesis: contradiction
now :: thesis: ( ( p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p4 `2 & contradiction ) or ( p4 in LSeg (|[(- 1),1]|,|[1,1]|) & contradiction ) or ( p4 in LSeg (|[1,1]|,|[1,(- 1)]|) & contradiction ) or ( p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p4 <> W-min (rectangle ((- 1),1,(- 1),1)) & contradiction ) )
per cases ( ( 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 A50;
case ( p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p4 `2 ) ; :: thesis: contradiction
end;
case p4 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: contradiction
end;
case p4 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: contradiction
end;
case A62: ( p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p4 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ; :: thesis: contradiction
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 ;
hence contradiction by A61, A62, A63, A65, TOPREAL3:6; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
case A66: ( not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) ; :: thesis: LE f . p4,f . p1,P
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 ;
now :: thesis: ( ( p4 `1 <> - 1 & LE f . p4,f . p1,P ) or ( p4 `1 = - 1 & p4 `2 >= 0 & LE f . p4,f . p1,P ) or ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 & LE f . p4,f . p1,P ) )
per cases ( p4 `1 <> - 1 or ( p4 `1 = - 1 & p4 `2 >= 0 ) or ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 ) ) by A66;
case A68: p4 `1 <> - 1 ; :: thesis: LE f . p4,f . p1,P
A69: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A70: dom f = the carrier of () 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 () : ( p in P & p `2 >= 0 ) } by ;
A73: f . p1 in P by ;
Lower_Arc P = { p where p is Point of () : ( p in P & p `2 <= 0 ) } by ;
then A74: f . p1 in Lower_Arc P by ;
A75: f . |[(- 1),0]| = W-min P by ;
A76: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
now :: thesis: ( ( p4 in LSeg (|[(- 1),1]|,|[1,1]|) & LE f . p4,f . p1,P ) or ( p4 in LSeg (|[1,1]|,|[1,(- 1)]|) & LE f . p4,f . p1,P ) or ( p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & LE f . p4,f . p1,P ) )
per cases ( p4 in LSeg (|[(- 1),1]|,|[1,1]|) or p4 in LSeg (|[1,1]|,|[1,(- 1)]|) or p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ) by ;
case p4 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: LE f . p4,f . p1,P
then A77: p4 `2 = 1 by Th3;
A78: f . p4 in P by ;
(f . p4) `2 >= 0 by ;
then f . p4 in Upper_Arc P by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
case p4 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: LE f . p4,f . p1,P
then A79: p4 `1 = 1 by Th1;
A80: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A81: dom f = the carrier of () by FUNCT_2:def 1;
then A82: f . p4 in P by ;
A83: f . p1 in P by ;
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 ;
A87: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
A88: (f . p4) `1 >= 0 by ;
now :: thesis: ( ( (f . p4) `2 >= 0 & LE f . p4,f . p1,P ) or ( (f . p4) `2 < 0 & LE f . p4,f . p1,P ) )
per cases ( (f . p4) `2 >= 0 or (f . p4) `2 < 0 ) ;
case A89: (f . p4) `2 >= 0 ; :: thesis: LE f . p4,f . p1,P
A90: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A91: Upper_Arc P = { p where p is Point of () : ( p in P & p `2 >= 0 ) } by ;
A92: f . |[(- 1),0]| = W-min P by ;
A93: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
A94: f . p4 in Upper_Arc P by ;
Lower_Arc P = { p where p is Point of () : ( p in P & p `2 <= 0 ) } by ;
then f . p1 in Lower_Arc P by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
case (f . p4) `2 < 0 ; :: thesis: LE f . p4,f . p1,P
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
end;
end;
hence LE f . p4,f . p1,P ; :: thesis: verum
end;
case A95: p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis: LE f . p4,f . p1,P
then p4 `2 = - 1 by Th3;
then A96: (f . p4) `2 < 0 by ;
A97: f . p4 in P by ;
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 ; :: thesis: verum
end;
end;
end;
hence LE f . p4,f . p1,P ; :: thesis: verum
end;
case A99: ( p4 `1 = - 1 & p4 `2 >= 0 ) ; :: thesis: LE f . p4,f . p1,P
A100: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A101: dom f = the carrier of () by FUNCT_2:def 1;
then A102: f . p4 in P by ;
A103: f . p1 in P by ;
A104: (f . p4) `2 >= 0 by ;
A105: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A106: Upper_Arc P = { p where p is Point of () : ( p in P & p `2 >= 0 ) } by ;
A107: f . |[(- 1),0]| = W-min P by ;
A108: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
A109: f . p4 in Upper_Arc P by ;
Lower_Arc P = { p where p is Point of () : ( p in P & p `2 <= 0 ) } by ;
then f . p1 in Lower_Arc P by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
case A110: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 ) ; :: thesis: LE f . p4,f . p1,P
then A111: p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by ;
A112: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A113: dom f = the carrier of () by FUNCT_2:def 1;
then A114: f . p4 in P by ;
A115: f . p1 in P by ;
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 ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
end;
end;
hence LE f . p4,f . p1,P ; :: thesis: verum
end;
end;
end;
A119: rectangle ((- 1),1,(- 1),1) = { p where p is Point of () : ( ( 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 () : ( ( 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: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
proof
thus rectangle ((- 1),1,(- 1),1) c= { p where p is Point of () : ( ( 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: { p where p is Point of () : ( ( 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)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rectangle ((- 1),1,(- 1),1) or x in { p where p is Point of () : ( ( 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 ) ) } )
assume x in rectangle ((- 1),1,(- 1),1) ; :: thesis: x in { p where p is Point of () : ( ( 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 ) ) }
then ex p being Point of () 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 () : ( ( 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: verum
end;
thus { p where p is Point of () : ( ( 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: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of () : ( ( 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 ) ) } or x in rectangle ((- 1),1,(- 1),1) )
assume x in { p where p is Point of () : ( ( 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: x in rectangle ((- 1),1,(- 1),1)
then ex p being Point of () 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: verum
end;
end;
thus f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by ; :: thesis: verum
end;
end;
end;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis: verum
end;
case A120: ( not p3 `2 < 0 or not p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis: ( rectangle ((- 1),1,(- 1),1) = { p where p is Point of () : ( ( 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 ) ) } & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P )
A121: now :: thesis: ( ( p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & ( ( 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)) ) ) ) or ( p3 in LSeg (|[(- 1),1]|,|[1,1]|) & ( ( 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)) ) ) ) or ( p3 in LSeg (|[1,1]|,|[1,(- 1)]|) & ( ( 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)) ) ) ) or ( p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & ( ( 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)) ) ) ) )
per cases ( p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) or p3 in LSeg (|[(- 1),1]|,|[1,1]|) or p3 in LSeg (|[1,1]|,|[1,(- 1)]|) or p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ) by ;
case p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ; :: thesis: ( ( 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)) ) )
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 ; :: thesis: verum
end;
case p3 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: ( ( 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)) ) )
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)) ) ) ; :: thesis: verum
end;
case p3 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: ( ( 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)) ) )
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)) ) ) ; :: thesis: verum
end;
case A122: p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis: ( ( 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)) ) )
A123: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;
now :: thesis: not p3 = W-min (rectangle ((- 1),1,(- 1),1))
assume A124: p3 = W-min (rectangle ((- 1),1,(- 1),1)) ; :: thesis: contradiction
then p3 `2 = - 1 by ;
hence contradiction by A120, A123, A124, RLTOPSP1:68; :: thesis: verum
end;
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 A122; :: thesis: verum
end;
end;
end;
then A125: LE |[(- 1),0]|,p3, rectangle ((- 1),1,(- 1),1) by ;
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 ;
A129: LE f . p3,f . p4,P by ;
A130: now :: thesis: ( ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 & contradiction ) or ( ( not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) & LE f . p4,f . p1,P ) )
per cases ( ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 ) or not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) ;
case A131: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 ) ; :: thesis: contradiction
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 ;
then A136: p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by ;
now :: thesis: ( ( p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p3 `2 & contradiction ) or ( p3 in LSeg (|[(- 1),1]|,|[1,1]|) & contradiction ) or ( p3 in LSeg (|[1,1]|,|[1,(- 1)]|) & contradiction ) or ( p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p3 <> W-min (rectangle ((- 1),1,(- 1),1)) & contradiction ) )
per cases ( ( 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 A121;
case A137: ( p3 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p3 `2 ) ; :: thesis: contradiction
end;
case A138: p3 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: contradiction
then LE p4,p3, rectangle ((- 1),1,(- 1),1) by ;
then p3 = p4 by ;
hence contradiction by A131, A138, Th3; :: thesis: verum
end;
case A139: p3 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: contradiction
then LE p4,p3, rectangle ((- 1),1,(- 1),1) by ;
then p3 = p4 by ;
hence contradiction by A131, A139, Th1; :: thesis: verum
end;
case A140: ( p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p3 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ; :: thesis: contradiction
then LE p4,p3, rectangle ((- 1),1,(- 1),1) by ;
then A141: p3 = p4 by ;
A142: p3 `2 = - 1 by ;
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 ;
hence contradiction by A131, A140, A141, A142, A144, TOPREAL3:6; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
case A145: ( not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) ; :: thesis: LE f . p4,f . p1,P
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 ;
now :: thesis: ( ( p4 `1 <> - 1 & LE f . p4,f . p1,P ) or ( p4 `1 = - 1 & p4 `2 >= 0 & LE f . p4,f . p1,P ) or ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 & LE f . p4,f . p1,P ) )
per cases ( p4 `1 <> - 1 or ( p4 `1 = - 1 & p4 `2 >= 0 ) or ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 ) ) by A145;
case A147: p4 `1 <> - 1 ; :: thesis: LE f . p4,f . p1,P
A148: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A149: dom f = the carrier of () 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 () : ( p in P & p `2 >= 0 ) } by ;
A152: f . p1 in P by ;
Lower_Arc P = { p where p is Point of () : ( p in P & p `2 <= 0 ) } by ;
then A153: f . p1 in Lower_Arc P by ;
A154: f . |[(- 1),0]| = W-min P by ;
A155: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
now :: thesis: ( ( p4 in LSeg (|[(- 1),1]|,|[1,1]|) & LE f . p4,f . p1,P ) or ( p4 in LSeg (|[1,1]|,|[1,(- 1)]|) & LE f . p4,f . p1,P ) or ( p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & LE f . p4,f . p1,P ) )
per cases ( p4 in LSeg (|[(- 1),1]|,|[1,1]|) or p4 in LSeg (|[1,1]|,|[1,(- 1)]|) or p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ) by ;
case p4 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: LE f . p4,f . p1,P
then A156: p4 `2 = 1 by Th3;
A157: f . p4 in P by ;
(f . p4) `2 >= 0 by ;
then f . p4 in Upper_Arc P by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
case p4 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: LE f . p4,f . p1,P
then A158: p4 `1 = 1 by Th1;
A159: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A160: dom f = the carrier of () by FUNCT_2:def 1;
then A161: f . p4 in P by ;
A162: f . p1 in P by ;
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 ;
A166: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
A167: (f . p4) `1 >= 0 by ;
now :: thesis: ( ( (f . p4) `2 >= 0 & LE f . p4,f . p1,P ) or ( (f . p4) `2 < 0 & LE f . p4,f . p1,P ) )
per cases ( (f . p4) `2 >= 0 or (f . p4) `2 < 0 ) ;
case A168: (f . p4) `2 >= 0 ; :: thesis: LE f . p4,f . p1,P
A169: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A170: Upper_Arc P = { p where p is Point of () : ( p in P & p `2 >= 0 ) } by ;
A171: f . |[(- 1),0]| = W-min P by ;
A172: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
A173: f . p4 in Upper_Arc P by ;
Lower_Arc P = { p where p is Point of () : ( p in P & p `2 <= 0 ) } by ;
then f . p1 in Lower_Arc P by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
case (f . p4) `2 < 0 ; :: thesis: LE f . p4,f . p1,P
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
end;
end;
hence LE f . p4,f . p1,P ; :: thesis: verum
end;
case A174: p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis: LE f . p4,f . p1,P
then p4 `2 = - 1 by Th3;
then A175: (f . p4) `2 < 0 by ;
A176: f . p4 in P by ;
A177: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
(f . p4) `1 >= (f . p1) `1 by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
end;
end;
hence LE f . p4,f . p1,P ; :: thesis: verum
end;
case A178: ( p4 `1 = - 1 & p4 `2 >= 0 ) ; :: thesis: LE f . p4,f . p1,P
A179: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A180: dom f = the carrier of () by FUNCT_2:def 1;
then A181: f . p4 in P by ;
A182: f . p1 in P by ;
A183: (f . p4) `2 >= 0 by ;
A184: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A185: Upper_Arc P = { p where p is Point of () : ( p in P & p `2 >= 0 ) } by ;
A186: f . |[(- 1),0]| = W-min P by ;
A187: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
A188: f . p4 in Upper_Arc P by ;
Lower_Arc P = { p where p is Point of () : ( p in P & p `2 <= 0 ) } by ;
then f . p1 in Lower_Arc P by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
case A189: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 ) ; :: thesis: LE f . p4,f . p1,P
then A190: p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by ;
A191: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A192: dom f = the carrier of () by FUNCT_2:def 1;
then A193: f . p4 in P by ;
A194: f . p1 in P by ;
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 ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
end;
end;
hence LE f . p4,f . p1,P ; :: thesis: verum
end;
end;
end;
A198: rectangle ((- 1),1,(- 1),1) = { p where p is Point of () : ( ( 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 () : ( ( 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: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
proof
thus rectangle ((- 1),1,(- 1),1) c= { p where p is Point of () : ( ( 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: { p where p is Point of () : ( ( 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)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rectangle ((- 1),1,(- 1),1) or x in { p where p is Point of () : ( ( 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 ) ) } )
assume x in rectangle ((- 1),1,(- 1),1) ; :: thesis: x in { p where p is Point of () : ( ( 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 ) ) }
then ex p being Point of () 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 () : ( ( 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: verum
end;
thus { p where p is Point of () : ( ( 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: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of () : ( ( 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 ) ) } or x in rectangle ((- 1),1,(- 1),1) )
assume x in { p where p is Point of () : ( ( 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: x in rectangle ((- 1),1,(- 1),1)
then ex p being Point of () 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 A198; :: thesis: verum
end;
end;
thus f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by ; :: thesis: verum
end;
end;
end;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis: verum
end;
case A199: ( not p2 `2 < 0 or not p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ) ; :: thesis: ( rectangle ((- 1),1,(- 1),1) = { p where p is Point of () : ( ( 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 ) ) } & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P )
A200: now :: thesis: ( ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & ( ( 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)) ) ) ) or ( p2 in LSeg (|[(- 1),1]|,|[1,1]|) & ( ( 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)) ) ) ) or ( p2 in LSeg (|[1,1]|,|[1,(- 1)]|) & ( ( 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)) ) ) ) or ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & ( ( 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)) ) ) ) )
per cases ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) or p2 in LSeg (|[(- 1),1]|,|[1,1]|) or p2 in LSeg (|[1,1]|,|[1,(- 1)]|) or p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ) by ;
case p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) ; :: thesis: ( ( 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)) ) )
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 ; :: thesis: verum
end;
case p2 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: ( ( 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)) ) )
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)) ) ) ; :: thesis: verum
end;
case p2 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: ( ( 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)) ) )
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)) ) ) ; :: thesis: verum
end;
case A201: p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis: ( ( 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)) ) )
A202: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;
now :: thesis: not p2 = W-min (rectangle ((- 1),1,(- 1),1))
assume A203: p2 = W-min (rectangle ((- 1),1,(- 1),1)) ; :: thesis: contradiction
then p2 `2 = - 1 by ;
hence contradiction by A199, A202, A203, RLTOPSP1:68; :: thesis: verum
end;
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 A201; :: thesis: verum
end;
end;
end;
then A204: LE |[(- 1),0]|,p2, rectangle ((- 1),1,(- 1),1) by ;
then A205: LE f . p2,f . p3,P by ;
LE |[(- 1),0]|,p3, rectangle ((- 1),1,(- 1),1) by ;
then A206: LE f . p3,f . p4,P by ;
A207: now :: thesis: ( ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 & contradiction ) or ( ( not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) & LE f . p4,f . p1,P ) )
per cases ( ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 ) or not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) ;
case A208: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 <= p4 `2 ) ; :: thesis: contradiction
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 ;
then A213: p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by ;
now :: thesis: ( ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p2 `2 & contradiction ) or ( p2 in LSeg (|[(- 1),1]|,|[1,1]|) & contradiction ) or ( p2 in LSeg (|[1,1]|,|[1,(- 1)]|) & contradiction ) or ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> W-min (rectangle ((- 1),1,(- 1),1)) & contradiction ) )
per cases ( ( 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 A200;
case A214: ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & |[(- 1),0]| `2 <= p2 `2 ) ; :: thesis: contradiction
end;
case A215: p2 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: contradiction
then LE p4,p2, rectangle ((- 1),1,(- 1),1) by ;
then p2 = p4 by ;
hence contradiction by A208, A215, Th3; :: thesis: verum
end;
case A216: p2 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: contradiction
then LE p4,p2, rectangle ((- 1),1,(- 1),1) by ;
then p2 = p4 by ;
hence contradiction by A208, A216, Th1; :: thesis: verum
end;
case A217: ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ; :: thesis: contradiction
then LE p4,p2, rectangle ((- 1),1,(- 1),1) by ;
then A218: p2 = p4 by ;
A219: p2 `2 = - 1 by ;
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 ;
hence contradiction by A208, A217, A218, A219, A221, TOPREAL3:6; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
case A222: ( not p4 `1 = - 1 or not p4 `2 < 0 or not p1 `2 <= p4 `2 ) ; :: thesis: LE f . p4,f . p1,P
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 ;
now :: thesis: ( ( p4 `1 <> - 1 & LE f . p4,f . p1,P ) or ( p4 `1 = - 1 & p4 `2 >= 0 & LE f . p4,f . p1,P ) or ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 & LE f . p4,f . p1,P ) )
per cases ( p4 `1 <> - 1 or ( p4 `1 = - 1 & p4 `2 >= 0 ) or ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 ) ) by A222;
case A224: p4 `1 <> - 1 ; :: thesis: LE f . p4,f . p1,P
A225: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A226: dom f = the carrier of () 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 () : ( p in P & p `2 >= 0 ) } by ;
A229: f . p1 in P by ;
Lower_Arc P = { p where p is Point of () : ( p in P & p `2 <= 0 ) } by ;
then A230: f . p1 in Lower_Arc P by ;
A231: f . |[(- 1),0]| = W-min P by ;
A232: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
now :: thesis: ( ( p4 in LSeg (|[(- 1),1]|,|[1,1]|) & LE f . p4,f . p1,P ) or ( p4 in LSeg (|[1,1]|,|[1,(- 1)]|) & LE f . p4,f . p1,P ) or ( p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & LE f . p4,f . p1,P ) )
per cases ( p4 in LSeg (|[(- 1),1]|,|[1,1]|) or p4 in LSeg (|[1,1]|,|[1,(- 1)]|) or p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ) by ;
case p4 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: LE f . p4,f . p1,P
then A233: p4 `2 = 1 by Th3;
A234: f . p4 in P by ;
(f . p4) `2 >= 0 by ;
then f . p4 in Upper_Arc P by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
case p4 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: LE f . p4,f . p1,P
then A235: p4 `1 = 1 by Th1;
A236: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A237: dom f = the carrier of () by FUNCT_2:def 1;
then A238: f . p4 in P by ;
A239: f . p1 in P by ;
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 ;
A243: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
A244: (f . p4) `1 >= 0 by ;
now :: thesis: ( ( (f . p4) `2 >= 0 & LE f . p4,f . p1,P ) or ( (f . p4) `2 < 0 & LE f . p4,f . p1,P ) )
per cases ( (f . p4) `2 >= 0 or (f . p4) `2 < 0 ) ;
case A245: (f . p4) `2 >= 0 ; :: thesis: LE f . p4,f . p1,P
A246: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A247: Upper_Arc P = { p where p is Point of () : ( p in P & p `2 >= 0 ) } by ;
A248: f . |[(- 1),0]| = W-min P by ;
A249: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
A250: f . p4 in Upper_Arc P by ;
Lower_Arc P = { p where p is Point of () : ( p in P & p `2 <= 0 ) } by ;
then f . p1 in Lower_Arc P by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
case (f . p4) `2 < 0 ; :: thesis: LE f . p4,f . p1,P
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
end;
end;
hence LE f . p4,f . p1,P ; :: thesis: verum
end;
case A251: p4 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) ; :: thesis: LE f . p4,f . p1,P
then p4 `2 = - 1 by Th3;
then A252: (f . p4) `2 < 0 by ;
A253: f . p4 in P by ;
A254: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
(f . p4) `1 >= (f . p1) `1 by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
end;
end;
hence LE f . p4,f . p1,P ; :: thesis: verum
end;
case A255: ( p4 `1 = - 1 & p4 `2 >= 0 ) ; :: thesis: LE f . p4,f . p1,P
A256: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A257: dom f = the carrier of () by FUNCT_2:def 1;
then A258: f . p4 in P by ;
A259: f . p1 in P by ;
A260: (f . p4) `2 >= 0 by ;
A261: (f . p1) `2 <= 0 by A2, A21, A29, Th67;
A262: Upper_Arc P = { p where p is Point of () : ( p in P & p `2 >= 0 ) } by ;
A263: f . |[(- 1),0]| = W-min P by ;
A264: now :: thesis: not f . p1 = W-min P
assume f . p1 = W-min P ; :: thesis: contradiction
then p1 = |[(- 1),0]| by ;
hence contradiction by A29, EUCLID:52; :: thesis: verum
end;
A265: f . p4 in Upper_Arc P by ;
Lower_Arc P = { p where p is Point of () : ( p in P & p `2 <= 0 ) } by ;
then f . p1 in Lower_Arc P by ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
case A266: ( p4 `1 = - 1 & p4 `2 < 0 & p1 `2 > p4 `2 ) ; :: thesis: LE f . p4,f . p1,P
then A267: p4 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) by ;
A268: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A269: dom f = the carrier of () by FUNCT_2:def 1;
then A270: f . p4 in P by ;
A271: f . p1 in P by ;
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 ;
hence LE f . p4,f . p1,P by ; :: thesis: verum
end;
end;
end;
hence LE f . p4,f . p1,P ; :: thesis: verum
end;
end;
end;
A275: rectangle ((- 1),1,(- 1),1) = { p where p is Point of () : ( ( 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 () : ( ( 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: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
proof
thus rectangle ((- 1),1,(- 1),1) c= { p where p is Point of () : ( ( 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: { p where p is Point of () : ( ( 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)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rectangle ((- 1),1,(- 1),1) or x in { p where p is Point of () : ( ( 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 ) ) } )
assume x in rectangle ((- 1),1,(- 1),1) ; :: thesis: x in { p where p is Point of () : ( ( 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 ) ) }
then ex p being Point of () 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 () : ( ( 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: verum
end;
thus { p where p is Point of () : ( ( 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: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of () : ( ( 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 ) ) } or x in rectangle ((- 1),1,(- 1),1) )
assume x in { p where p is Point of () : ( ( 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: x in rectangle ((- 1),1,(- 1),1)
then ex p being Point of () 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 A275; :: thesis: verum
end;
end;
thus f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by ; :: thesis: verum
end;
end;
end;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis: verum
end;
end;
end;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis: verum
end;
case A276: p1 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
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 ;
then A280: LE |[(- 1),1]|,p1, rectangle ((- 1),1,(- 1),1) by ;
then A281: LE f . p1,f . p2,P by ;
A282: LE |[(- 1),1]|,p2, rectangle ((- 1),1,(- 1),1) by ;
then A283: LE f . p2,f . p3,P by ;
LE |[(- 1),1]|,p3, rectangle ((- 1),1,(- 1),1) by ;
then LE f . p3,f . p4,P by ;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by ; :: thesis: verum
end;
case A284: p1 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
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 ;
p1 `2 <= 1 by ;
then LE |[1,1]|,p1, rectangle ((- 1),1,(- 1),1) by ;
then A293: LE |[(- 1),1]|,p1, rectangle ((- 1),1,(- 1),1) by ;
then A294: LE f . p1,f . p2,P by ;
A295: LE |[(- 1),1]|,p2, rectangle ((- 1),1,(- 1),1) by ;
then A296: LE f . p2,f . p3,P by ;
LE |[(- 1),1]|,p3, rectangle ((- 1),1,(- 1),1) by ;
then LE f . p3,f . p4,P by ;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by ; :: thesis: verum
end;
case A297: ( p1 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p1 <> W-min (rectangle ((- 1),1,(- 1),1)) ) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
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 ;
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 ;
then A306: LE |[(- 1),1]|,|[1,(- 1)]|, rectangle ((- 1),1,(- 1),1) by ;
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 ;
then LE |[1,(- 1)]|,p1, rectangle ((- 1),1,(- 1),1) by ;
then A308: LE |[(- 1),1]|,p1, rectangle ((- 1),1,(- 1),1) by ;
then A309: LE f . p1,f . p2,P by ;
A310: LE |[(- 1),1]|,p2, rectangle ((- 1),1,(- 1),1) by ;
then A311: LE f . p2,f . p3,P by ;
LE |[(- 1),1]|,p3, rectangle ((- 1),1,(- 1),1) by ;
then LE f . p3,f . p4,P by ;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by ; :: thesis: verum
end;
end;
end;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis: verum
end;