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 f . p1,f . p2,P & LE f . p2,f . p3,P & LE f . p3,f . p4,P holds
p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1)

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

let f be Function of (),(); :: thesis: ( P = circle (0,0,1) & f = Sq_Circ & LE f . p1,f . p2,P & LE f . p2,f . p3,P & LE f . p3,f . p4,P implies p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) )
set K = rectangle ((- 1),1,(- 1),1);
assume that
A1: P = circle (0,0,1) and
A2: f = Sq_Circ and
A3: LE f . p1,f . p2,P and
A4: LE f . p2,f . p3,P and
A5: LE f . p3,f . p4,P ; :: thesis: p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1)
A6: rectangle ((- 1),1,(- 1),1) is being_simple_closed_curve by Th50;
A7: P = { p where p is Point of () : |.p.| = 1 } by ;
then A8: LE f . p1,f . p3,P by ;
A9: LE f . p2,f . p4,P by ;
A10: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A11: dom f = the carrier of () by FUNCT_2:def 1;
A12: P = { p where p is Point of () : |.p.| = 1 } by ;
then A13: P is being_simple_closed_curve by JGRAPH_3:26;
then f . p1 in P by ;
then ex x1 being object st
( x1 in dom f & x1 in rectangle ((- 1),1,(- 1),1) & f . p1 = f . x1 ) by ;
then A14: p1 in rectangle ((- 1),1,(- 1),1) by ;
f . p2 in P by ;
then ex x2 being object st
( x2 in dom f & x2 in rectangle ((- 1),1,(- 1),1) & f . p2 = f . x2 ) by ;
then A15: p2 in rectangle ((- 1),1,(- 1),1) by ;
f . p3 in P by ;
then ex x3 being object st
( x3 in dom f & x3 in rectangle ((- 1),1,(- 1),1) & f . p3 = f . x3 ) by ;
then A16: p3 in rectangle ((- 1),1,(- 1),1) by ;
f . p4 in P by ;
then ex x4 being object st
( x4 in dom f & x4 in rectangle ((- 1),1,(- 1),1) & f . p4 = f . x4 ) by ;
then A17: p4 in rectangle ((- 1),1,(- 1),1) by ;
now :: thesis: p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1)
assume A18: not p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ; :: thesis: contradiction
A19: now :: thesis: not p1,p2,p4,p3 are_in_this_order_on rectangle ((- 1),1,(- 1),1)
assume A20: p1,p2,p4,p3 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ; :: thesis: contradiction
now :: thesis: ( ( LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p2, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) & contradiction ) )
per cases ( ( LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) ) or ( LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) ) or ( LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p2, rectangle ((- 1),1,(- 1),1) ) or ( LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) ) ) by ;
case A21: ( LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p1,f . p2,f . p4,f . p3 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p1,f . p2,P & LE f . p2,f . p4,P & LE f . p4,f . p3,P ) or ( LE f . p2,f . p4,P & LE f . p4,f . p3,P & LE f . p3,f . p1,P ) or ( LE f . p4,f . p3,P & LE f . p3,f . p1,P & LE f . p1,f . p2,P ) or ( LE f . p3,f . p1,P & LE f . p1,f . p2,P & LE f . p2,f . p4,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p4 or f . p3 = f . p1 ) by ;
then A22: ( p3 = p4 or p3 = p1 ) by ;
LE p1,p4, rectangle ((- 1),1,(- 1),1) by ;
then p1 = p4 by ;
hence contradiction by A18, A20, A22; :: thesis: verum
end;
case A23: ( LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p2,f . p4,f . p3,f . p1 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p2,f . p4,P & LE f . p4,f . p3,P & LE f . p3,f . p1,P ) or ( LE f . p4,f . p3,P & LE f . p3,f . p1,P & LE f . p1,f . p2,P ) or ( LE f . p3,f . p1,P & LE f . p1,f . p2,P & LE f . p2,f . p4,P ) or ( LE f . p1,f . p2,P & LE f . p2,f . p4,P & LE f . p4,f . p3,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p4 or LE f . p3,f . p2,P ) by ;
then ( f . p3 = f . p4 or f . p3 = f . p2 ) by ;
then A24: ( p3 = p4 or p3 = p2 ) by ;
then p4 = p2 by ;
hence contradiction by A18, A20, A24; :: thesis: verum
end;
case A25: ( LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p2, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p4,f . p3,f . p1,f . p2 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p4,f . p3,P & LE f . p3,f . p1,P & LE f . p1,f . p2,P ) or ( LE f . p3,f . p1,P & LE f . p1,f . p2,P & LE f . p2,f . p4,P ) or ( LE f . p1,f . p2,P & LE f . p2,f . p4,P & LE f . p4,f . p3,P ) or ( LE f . p2,f . p4,P & LE f . p4,f . p3,P & LE f . p3,f . p1,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p4 or LE f . p3,f . p2,P ) by ;
then ( f . p3 = f . p4 or f . p3 = f . p2 ) by ;
then A26: ( p3 = p4 or p3 = p2 ) by ;
then p3 = p1 by ;
hence contradiction by A6, A18, A20, A26, JORDAN17:12; :: thesis: verum
end;
case A27: ( LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p3,f . p1,f . p2,f . p4 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p4,f . p3,P & LE f . p3,f . p1,P & LE f . p1,f . p2,P ) or ( LE f . p3,f . p1,P & LE f . p1,f . p2,P & LE f . p2,f . p4,P ) or ( LE f . p1,f . p2,P & LE f . p2,f . p4,P & LE f . p4,f . p3,P ) or ( LE f . p2,f . p4,P & LE f . p4,f . p3,P & LE f . p3,f . p1,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p4 or LE f . p3,f . p2,P ) by ;
then ( f . p3 = f . p4 or f . p3 = f . p2 ) by ;
then A28: ( p3 = p4 or p3 = p2 ) by ;
then p3 = p1 by ;
hence contradiction by A6, A18, A20, A28, JORDAN17:12; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
A29: now :: thesis: not p1,p3,p4,p2 are_in_this_order_on rectangle ((- 1),1,(- 1),1)
assume A30: p1,p3,p4,p2 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ; :: thesis: contradiction
now :: thesis: ( ( LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p3,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) & contradiction ) )
per cases ( ( LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) ) or ( LE p3,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) ) or ( LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) ) or ( LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) ) ) by ;
case ( LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p1,f . p3,f . p4,f . p2 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p1,f . p3,P & LE f . p3,f . p4,P & LE f . p4,f . p2,P ) or ( LE f . p3,f . p4,P & LE f . p4,f . p2,P & LE f . p2,f . p1,P ) or ( LE f . p4,f . p2,P & LE f . p2,f . p1,P & LE f . p1,f . p3,P ) or ( LE f . p2,f . p1,P & LE f . p1,f . p3,P & LE f . p3,f . p4,P ) ) by JORDAN17:def 1;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by ;
then A31: ( p4 = p2 or p2 = p1 ) by ;
then ( f . p3 = f . p2 or f . p4 = f . p1 ) by ;
then ( p3 = p2 or p4 = p1 ) by ;
hence contradiction by A6, A18, A30, A31, JORDAN17:12; :: thesis: verum
end;
case ( LE p3,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p3,f . p4,f . p2,f . p1 are_in_this_order_on P by A1, A2, Th72;
then A32: ( ( LE f . p1,f . p3,P & LE f . p3,f . p4,P & LE f . p4,f . p2,P ) or ( LE f . p3,f . p4,P & LE f . p4,f . p2,P & LE f . p2,f . p1,P ) or ( LE f . p4,f . p2,P & LE f . p2,f . p1,P & LE f . p1,f . p3,P ) or ( LE f . p2,f . p1,P & LE f . p1,f . p3,P & LE f . p3,f . p4,P ) ) by JORDAN17:def 1;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by ;
then A33: ( p4 = p2 or p2 = p1 ) by ;
( f . p2 = f . p1 or LE f . p3,f . p2,P ) by ;
then ( f . p2 = f . p1 or f . p3 = f . p2 ) by ;
then ( p2 = p1 or p3 = p2 ) by ;
hence contradiction by A6, A18, A30, A33, JORDAN17:12; :: thesis: verum
end;
case ( LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p4,f . p2,f . p1,f . p3 are_in_this_order_on P by A1, A2, Th72;
then A34: ( ( LE f . p1,f . p3,P & LE f . p3,f . p4,P & LE f . p4,f . p2,P ) or ( LE f . p3,f . p4,P & LE f . p4,f . p2,P & LE f . p2,f . p1,P ) or ( LE f . p4,f . p2,P & LE f . p2,f . p1,P & LE f . p1,f . p3,P ) or ( LE f . p2,f . p1,P & LE f . p1,f . p3,P & LE f . p3,f . p4,P ) ) by JORDAN17:def 1;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by ;
then A35: ( p4 = p2 or p2 = p1 ) by ;
( f . p2 = f . p1 or LE f . p3,f . p2,P ) by ;
then ( f . p2 = f . p1 or f . p3 = f . p2 ) by ;
then ( p2 = p1 or p3 = p2 ) by ;
hence contradiction by A6, A18, A30, A35, JORDAN17:12; :: thesis: verum
end;
case A36: ( LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p2,f . p1,f . p3,f . p4 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p1,f . p3,P & LE f . p3,f . p4,P & LE f . p4,f . p2,P ) or ( LE f . p3,f . p4,P & LE f . p4,f . p2,P & LE f . p2,f . p1,P ) or ( LE f . p4,f . p2,P & LE f . p2,f . p1,P & LE f . p1,f . p3,P ) or ( LE f . p2,f . p1,P & LE f . p1,f . p3,P & LE f . p3,f . p4,P ) ) by JORDAN17:def 1;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by ;
then A37: ( p4 = p2 or p2 = p1 ) by ;
LE p2,p3, rectangle ((- 1),1,(- 1),1) by ;
then p2 = p3 by ;
hence contradiction by A6, A18, A30, A37, JORDAN17:12; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
now :: thesis: ( ( p1,p2,p4,p3 are_in_this_order_on rectangle ((- 1),1,(- 1),1) & contradiction ) or ( p1,p3,p2,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) & contradiction ) or ( p1,p3,p4,p2 are_in_this_order_on rectangle ((- 1),1,(- 1),1) & contradiction ) or ( p1,p4,p2,p3 are_in_this_order_on rectangle ((- 1),1,(- 1),1) & contradiction ) or ( p1,p4,p3,p2 are_in_this_order_on rectangle ((- 1),1,(- 1),1) & contradiction ) )
per cases ( p1,p2,p4,p3 are_in_this_order_on rectangle ((- 1),1,(- 1),1) or p1,p3,p2,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) or p1,p3,p4,p2 are_in_this_order_on rectangle ((- 1),1,(- 1),1) or p1,p4,p2,p3 are_in_this_order_on rectangle ((- 1),1,(- 1),1) or p1,p4,p3,p2 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ) by ;
case A38: p1,p3,p2,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ; :: thesis: contradiction
now :: thesis: ( ( LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p1, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p4,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) & contradiction ) )
per cases ( ( LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) ) or ( LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p1, rectangle ((- 1),1,(- 1),1) ) or ( LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) ) or ( LE p4,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) ) ) by ;
case A39: ( LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p1,f . p3,f . p2,f . p4 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p1,f . p3,P & LE f . p3,f . p2,P & LE f . p2,f . p4,P ) or ( LE f . p3,f . p2,P & LE f . p2,f . p4,P & LE f . p4,f . p1,P ) or ( LE f . p2,f . p4,P & LE f . p4,f . p1,P & LE f . p1,f . p3,P ) or ( LE f . p4,f . p1,P & LE f . p1,f . p3,P & LE f . p3,f . p2,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p2 or LE f . p2,f . p1,P ) by ;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by ;
then A40: ( p3 = p2 or p2 = p1 ) by ;
then p3 = p1 by ;
hence contradiction by A18, A38, A40; :: thesis: verum
end;
case A41: ( LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p1, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p3,f . p2,f . p4,f . p1 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p1,f . p3,P & LE f . p3,f . p2,P & LE f . p2,f . p4,P ) or ( LE f . p3,f . p2,P & LE f . p2,f . p4,P & LE f . p4,f . p1,P ) or ( LE f . p2,f . p4,P & LE f . p4,f . p1,P & LE f . p1,f . p3,P ) or ( LE f . p4,f . p1,P & LE f . p1,f . p3,P & LE f . p3,f . p2,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p2 or LE f . p2,f . p1,P ) by ;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by ;
then A42: ( p3 = p2 or p2 = p1 ) by ;
then p4 = p1 by ;
hence contradiction by A6, A18, A38, A42, JORDAN17:12; :: thesis: verum
end;
case A43: ( LE p2,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p2,f . p4,f . p1,f . p3 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p1,f . p3,P & LE f . p3,f . p2,P & LE f . p2,f . p4,P ) or ( LE f . p3,f . p2,P & LE f . p2,f . p4,P & LE f . p4,f . p1,P ) or ( LE f . p2,f . p4,P & LE f . p4,f . p1,P & LE f . p1,f . p3,P ) or ( LE f . p4,f . p1,P & LE f . p1,f . p3,P & LE f . p3,f . p2,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p2 or LE f . p2,f . p1,P ) by ;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by ;
then A44: ( p3 = p2 or p2 = p1 ) by ;
then p4 = p1 by ;
hence contradiction by A6, A18, A38, A44, JORDAN17:12; :: thesis: verum
end;
case A45: ( LE p4,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p4,f . p1,f . p3,f . p2 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p1,f . p3,P & LE f . p3,f . p2,P & LE f . p2,f . p4,P ) or ( LE f . p3,f . p2,P & LE f . p2,f . p4,P & LE f . p4,f . p1,P ) or ( LE f . p2,f . p4,P & LE f . p4,f . p1,P & LE f . p1,f . p3,P ) or ( LE f . p4,f . p1,P & LE f . p1,f . p3,P & LE f . p3,f . p2,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p2 or LE f . p2,f . p1,P ) by ;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by ;
then A46: ( p3 = p2 or p2 = p1 ) by ;
then p3 = p1 by ;
hence contradiction by A18, A38, A46; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
case A47: p1,p4,p2,p3 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ; :: thesis: contradiction
now :: thesis: ( ( LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) & contradiction ) )
per cases ( ( LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) ) or ( LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) ) or ( LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) ) or ( LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) ) ) by ;
case A48: ( LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p1,f . p4,f . p2,f . p3 are_in_this_order_on P by A1, A2, Th72;
then A49: ( ( LE f . p1,f . p4,P & LE f . p4,f . p2,P & LE f . p2,f . p3,P ) or ( LE f . p4,f . p2,P & LE f . p2,f . p3,P & LE f . p3,f . p1,P ) or ( LE f . p2,f . p3,P & LE f . p3,f . p1,P & LE f . p1,f . p4,P ) or ( LE f . p3,f . p1,P & LE f . p1,f . p4,P & LE f . p4,f . p2,P ) ) by JORDAN17:def 1;
then ( f . p4 = f . p2 or LE f . p2,f . p1,P ) by ;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by ;
then A50: ( p4 = p2 or p2 = p1 ) by ;
then A51: p4 = p2 by ;
( f . p3 = f . p1 or LE f . p4,f . p3,P ) by ;
then ( f . p3 = f . p1 or f . p4 = f . p3 ) by ;
then A52: ( p3 = p1 or p4 = p3 ) by ;
then p1 = p2 by ;
hence contradiction by A18, A47, A51, A52; :: thesis: verum
end;
case A53: ( LE p4,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p4,f . p2,f . p3,f . p1 are_in_this_order_on P by A1, A2, Th72;
then A54: ( ( LE f . p1,f . p4,P & LE f . p4,f . p2,P & LE f . p2,f . p3,P ) or ( LE f . p4,f . p2,P & LE f . p2,f . p3,P & LE f . p3,f . p1,P ) or ( LE f . p2,f . p3,P & LE f . p3,f . p1,P & LE f . p1,f . p4,P ) or ( LE f . p3,f . p1,P & LE f . p1,f . p4,P & LE f . p4,f . p2,P ) ) by JORDAN17:def 1;
then ( f . p4 = f . p2 or LE f . p2,f . p1,P ) by ;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by ;
then ( p4 = p2 or p2 = p1 ) by ;
then A55: ( p4 = p2 or ( p2 = p1 & p3 = p1 ) ) by ;
( f . p3 = f . p1 or LE f . p4,f . p3,P ) by ;
then ( f . p3 = f . p1 or f . p4 = f . p3 ) by ;
then ( p3 = p1 or p4 = p3 ) by ;
hence contradiction by A6, A29, A47, A55, JORDAN17:12; :: thesis: verum
end;
case A56: ( LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p2,f . p3,f . p1,f . p4 are_in_this_order_on P by A1, A2, Th72;
then A57: ( ( LE f . p1,f . p4,P & LE f . p4,f . p2,P & LE f . p2,f . p3,P ) or ( LE f . p4,f . p2,P & LE f . p2,f . p3,P & LE f . p3,f . p1,P ) or ( LE f . p2,f . p3,P & LE f . p3,f . p1,P & LE f . p1,f . p4,P ) or ( LE f . p3,f . p1,P & LE f . p1,f . p4,P & LE f . p4,f . p2,P ) ) by JORDAN17:def 1;
then ( f . p4 = f . p2 or LE f . p2,f . p1,P ) by ;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by ;
then ( p4 = p2 or p2 = p1 ) by ;
then A58: ( p4 = p2 or ( p2 = p1 & p3 = p1 ) ) by ;
( f . p3 = f . p1 or LE f . p4,f . p3,P ) by ;
then ( f . p3 = f . p1 or f . p4 = f . p3 ) by ;
then ( p3 = p1 or p4 = p3 ) by ;
hence contradiction by A6, A29, A47, A58, JORDAN17:12; :: thesis: verum
end;
case A59: ( LE p3,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p2, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p3,f . p1,f . p4,f . p2 are_in_this_order_on P by A1, A2, Th72;
then A60: ( ( LE f . p1,f . p4,P & LE f . p4,f . p2,P & LE f . p2,f . p3,P ) or ( LE f . p4,f . p2,P & LE f . p2,f . p3,P & LE f . p3,f . p1,P ) or ( LE f . p2,f . p3,P & LE f . p3,f . p1,P & LE f . p1,f . p4,P ) or ( LE f . p3,f . p1,P & LE f . p1,f . p4,P & LE f . p4,f . p2,P ) ) by JORDAN17:def 1;
then ( f . p4 = f . p2 or LE f . p2,f . p1,P ) by ;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by ;
then ( p4 = p2 or p2 = p1 ) by ;
then A61: p4 = p2 by ;
( f . p3 = f . p1 or LE f . p4,f . p3,P ) by ;
then ( f . p3 = f . p1 or f . p4 = f . p3 ) by ;
then ( p3 = p1 or p4 = p3 ) by ;
hence contradiction by A6, A29, A47, A61, JORDAN17:12; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
case A62: p1,p4,p3,p2 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ; :: thesis: contradiction
now :: thesis: ( ( LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) & contradiction ) or ( LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) & contradiction ) )
per cases ( ( LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) ) or ( LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) ) or ( LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) ) or ( LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) ) ) by ;
case A63: ( LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p1,f . p4,f . p3,f . p2 are_in_this_order_on P by A1, A2, Th72;
then A64: ( ( LE f . p1,f . p4,P & LE f . p4,f . p3,P & LE f . p3,f . p2,P ) or ( LE f . p4,f . p3,P & LE f . p3,f . p2,P & LE f . p2,f . p1,P ) or ( LE f . p3,f . p2,P & LE f . p2,f . p1,P & LE f . p1,f . p4,P ) or ( LE f . p2,f . p1,P & LE f . p1,f . p4,P & LE f . p4,f . p3,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by ;
then A65: ( p3 = p2 or p2 = p1 ) by ;
LE p1,p3, rectangle ((- 1),1,(- 1),1) by ;
then A66: p3 = p2 by ;
( f . p4 = f . p3 or f . p2 = f . p1 ) by ;
then ( p4 = p3 or p2 = p1 ) by ;
then ( p4 = p3 or p2,p3,p4,p1 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ) by ;
hence contradiction by A6, A18, A62, A65, JORDAN17:12; :: thesis: verum
end;
case ( LE p4,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p4,f . p3,f . p2,f . p1 are_in_this_order_on P by A1, A2, Th72;
then A67: ( ( LE f . p1,f . p4,P & LE f . p4,f . p3,P & LE f . p3,f . p2,P ) or ( LE f . p4,f . p3,P & LE f . p3,f . p2,P & LE f . p2,f . p1,P ) or ( LE f . p3,f . p2,P & LE f . p2,f . p1,P & LE f . p1,f . p4,P ) or ( LE f . p2,f . p1,P & LE f . p1,f . p4,P & LE f . p4,f . p3,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by ;
then A68: ( p3 = p2 or p2 = p1 ) by ;
( f . p4 = f . p3 or f . p2 = f . p1 ) by ;
then ( p4 = p3 or p2 = p1 ) by ;
hence contradiction by A6, A19, A62, A68, JORDAN17:12; :: thesis: verum
end;
case ( LE p3,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p3,f . p2,f . p1,f . p4 are_in_this_order_on P by A1, A2, Th72;
then ( ( LE f . p1,f . p4,P & LE f . p4,f . p3,P & LE f . p3,f . p2,P ) or ( LE f . p4,f . p3,P & LE f . p3,f . p2,P & LE f . p2,f . p1,P ) or ( LE f . p3,f . p2,P & LE f . p2,f . p1,P & LE f . p1,f . p4,P ) or ( LE f . p2,f . p1,P & LE f . p1,f . p4,P & LE f . p4,f . p3,P ) ) by JORDAN17:def 1;
then ( f . p4 = f . p3 or f . p2 = f . p1 ) by ;
then ( p4 = p3 or p2 = p1 ) by ;
hence contradiction by A6, A19, A29, A62, JORDAN17:12; :: thesis: verum
end;
case A69: ( LE p2,p1, rectangle ((- 1),1,(- 1),1) & LE p1,p4, rectangle ((- 1),1,(- 1),1) & LE p4,p3, rectangle ((- 1),1,(- 1),1) ) ; :: thesis: contradiction
then f . p2,f . p1,f . p4,f . p3 are_in_this_order_on P by A1, A2, Th72;
then A70: ( ( LE f . p1,f . p4,P & LE f . p4,f . p3,P & LE f . p3,f . p2,P ) or ( LE f . p4,f . p3,P & LE f . p3,f . p2,P & LE f . p2,f . p1,P ) or ( LE f . p3,f . p2,P & LE f . p2,f . p1,P & LE f . p1,f . p4,P ) or ( LE f . p2,f . p1,P & LE f . p1,f . p4,P & LE f . p4,f . p3,P ) ) by JORDAN17:def 1;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by ;
then A71: ( p3 = p2 or p2 = p1 ) by ;
LE p1,p3, rectangle ((- 1),1,(- 1),1) by ;
then A72: p1 = p2 by ;
( f . p4 = f . p3 or f . p2 = f . p3 ) by ;
then ( p4 = p3 or p2 = p3 ) by ;
hence contradiction by A6, A29, A62, A72, JORDAN17:12; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ; :: thesis: verum