let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) 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 (TOP-REAL 2); :: thesis: for f being Function of (TOP-REAL 2),(TOP-REAL 2) 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 (TOP-REAL 2),(TOP-REAL 2); :: 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 (TOP-REAL 2) : |.p.| = 1 } by A1, Th24;
then A8: LE f . p1,f . p3,P by A3, A4, JGRAPH_3:26, JORDAN6:58;
A9: LE f . p2,f . p4,P by A4, A5, A7, JGRAPH_3:26, JORDAN6:58;
A10: f .: (rectangle ((- 1),1,(- 1),1)) = P by A2, A7, Lm15, Th35, JGRAPH_3:23;
A11: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A12: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } by A1, Th24;
then A13: P is being_simple_closed_curve by JGRAPH_3:26;
then f . p1 in P by A3, JORDAN7:5;
then ex x1 being object st
( x1 in dom f & x1 in rectangle ((- 1),1,(- 1),1) & f . p1 = f . x1 ) by A10, FUNCT_1:def 6;
then A14: p1 in rectangle ((- 1),1,(- 1),1) by A2, A11, FUNCT_1:def 4;
f . p2 in P by A3, A13, JORDAN7:5;
then ex x2 being object st
( x2 in dom f & x2 in rectangle ((- 1),1,(- 1),1) & f . p2 = f . x2 ) by A10, FUNCT_1:def 6;
then A15: p2 in rectangle ((- 1),1,(- 1),1) by A2, A11, FUNCT_1:def 4;
f . p3 in P by A4, A13, JORDAN7:5;
then ex x3 being object st
( x3 in dom f & x3 in rectangle ((- 1),1,(- 1),1) & f . p3 = f . x3 ) by A10, FUNCT_1:def 6;
then A16: p3 in rectangle ((- 1),1,(- 1),1) by A2, A11, FUNCT_1:def 4;
f . p4 in P by A5, A13, JORDAN7:5;
then ex x4 being object st
( x4 in dom f & x4 in rectangle ((- 1),1,(- 1),1) & f . p4 = f . x4 ) by A10, FUNCT_1:def 6;
then A17: p4 in rectangle ((- 1),1,(- 1),1) by A2, A11, FUNCT_1:def 4;
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 A20, JORDAN17:def 1;
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 A5, A8, A12, JGRAPH_3:26, JORDAN6:57;
then A22: ( p3 = p4 or p3 = p1 ) by A2, A11, FUNCT_1:def 4;
LE p1,p4, rectangle ((- 1),1,(- 1),1) by A21, Th50, JORDAN6:58;
then p1 = p4 by A18, A20, A21, A22, Th50, JORDAN6:57;
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 A5, A13, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p4 or f . p3 = f . p2 ) by A4, A12, JGRAPH_3:26, JORDAN6:57;
then A24: ( p3 = p4 or p3 = p2 ) by A2, A11, FUNCT_1:def 4;
then p4 = p2 by A18, A20, A23, Th50, JORDAN6:57;
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 A5, A13, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p4 or f . p3 = f . p2 ) by A4, A12, JGRAPH_3:26, JORDAN6:57;
then A26: ( p3 = p4 or p3 = p2 ) by A2, A11, FUNCT_1:def 4;
then p3 = p1 by A18, A20, A25, Th50, JORDAN6:57;
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 A5, A13, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p4 or f . p3 = f . p2 ) by A4, A12, JGRAPH_3:26, JORDAN6:57;
then A28: ( p3 = p4 or p3 = p2 ) by A2, A11, FUNCT_1:def 4;
then p3 = p1 by A18, A20, A27, Th50, JORDAN6:57;
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 A30, JORDAN17:def 1;
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 A3, A9, A12, JGRAPH_3:26, JORDAN6:57;
then A31: ( p4 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
then ( f . p3 = f . p2 or f . p4 = f . p1 ) by A4, A5, A6, A12, A18, A30, JGRAPH_3:26, JORDAN17:12, JORDAN6:57;
then ( p3 = p2 or p4 = p1 ) by A2, A11, FUNCT_1:def 4;
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 A3, A9, A12, JGRAPH_3:26, JORDAN6:57;
then A33: ( p4 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
( f . p2 = f . p1 or LE f . p3,f . p2,P ) by A3, A13, A32, JORDAN6:57, JORDAN6:58;
then ( f . p2 = f . p1 or f . p3 = f . p2 ) by A4, A12, JGRAPH_3:26, JORDAN6:57;
then ( p2 = p1 or p3 = p2 ) by A2, A11, FUNCT_1:def 4;
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 A3, A9, A12, JGRAPH_3:26, JORDAN6:57;
then A35: ( p4 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
( f . p2 = f . p1 or LE f . p3,f . p2,P ) by A3, A13, A34, JORDAN6:57, JORDAN6:58;
then ( f . p2 = f . p1 or f . p3 = f . p2 ) by A4, A12, JGRAPH_3:26, JORDAN6:57;
then ( p2 = p1 or p3 = p2 ) by A2, A11, FUNCT_1:def 4;
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 A3, A9, A12, JGRAPH_3:26, JORDAN6:57;
then A37: ( p4 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
LE p2,p3, rectangle ((- 1),1,(- 1),1) by A36, Th50, JORDAN6:58;
then p2 = p3 by A6, A18, A30, A36, A37, JORDAN17:12, JORDAN6:57;
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 A6, A14, A15, A16, A17, A18, JORDAN17:27;
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 A38, JORDAN17:def 1;
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 A4, A13, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by A3, A12, JGRAPH_3:26, JORDAN6:57;
then A40: ( p3 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
then p3 = p1 by A18, A38, A39, Th50, JORDAN6:57;
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 A4, A13, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by A3, A12, JGRAPH_3:26, JORDAN6:57;
then A42: ( p3 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
then p4 = p1 by A18, A38, A41, Th50, JORDAN6:57;
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 A4, A13, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by A3, A12, JGRAPH_3:26, JORDAN6:57;
then A44: ( p3 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
then p4 = p1 by A18, A38, A43, Th50, JORDAN6:57;
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 A4, A13, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p2 or f . p2 = f . p1 ) by A3, A12, JGRAPH_3:26, JORDAN6:57;
then A46: ( p3 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
then p3 = p1 by A18, A38, A45, Th50, JORDAN6:57;
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 A47, JORDAN17:def 1;
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 A9, A13, JORDAN6:57, JORDAN6:58;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by A3, A12, JGRAPH_3:26, JORDAN6:57;
then A50: ( p4 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
then A51: p4 = p2 by A48, Th50, JORDAN6:57;
( f . p3 = f . p1 or LE f . p4,f . p3,P ) by A8, A13, A49, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p1 or f . p4 = f . p3 ) by A5, A12, JGRAPH_3:26, JORDAN6:57;
then A52: ( p3 = p1 or p4 = p3 ) by A2, A11, FUNCT_1:def 4;
then p1 = p2 by A18, A47, A48, A50, Th50, JORDAN6:57;
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 A9, A13, JORDAN6:57, JORDAN6:58;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by A3, A12, JGRAPH_3:26, JORDAN6:57;
then ( p4 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
then A55: ( p4 = p2 or ( p2 = p1 & p3 = p1 ) ) by A53, Th50, JORDAN6:57;
( f . p3 = f . p1 or LE f . p4,f . p3,P ) by A8, A13, A54, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p1 or f . p4 = f . p3 ) by A5, A12, JGRAPH_3:26, JORDAN6:57;
then ( p3 = p1 or p4 = p3 ) by A2, A11, FUNCT_1:def 4;
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 A9, A13, JORDAN6:57, JORDAN6:58;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by A3, A12, JGRAPH_3:26, JORDAN6:57;
then ( p4 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
then A58: ( p4 = p2 or ( p2 = p1 & p3 = p1 ) ) by A56, Th50, JORDAN6:57;
( f . p3 = f . p1 or LE f . p4,f . p3,P ) by A8, A13, A57, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p1 or f . p4 = f . p3 ) by A5, A12, JGRAPH_3:26, JORDAN6:57;
then ( p3 = p1 or p4 = p3 ) by A2, A11, FUNCT_1:def 4;
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 A9, A13, JORDAN6:57, JORDAN6:58;
then ( f . p4 = f . p2 or f . p2 = f . p1 ) by A3, A12, JGRAPH_3:26, JORDAN6:57;
then ( p4 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
then A61: p4 = p2 by A59, Th50, JORDAN6:57;
( f . p3 = f . p1 or LE f . p4,f . p3,P ) by A8, A13, A60, JORDAN6:57, JORDAN6:58;
then ( f . p3 = f . p1 or f . p4 = f . p3 ) by A5, A12, JGRAPH_3:26, JORDAN6:57;
then ( p3 = p1 or p4 = p3 ) by A2, A11, FUNCT_1:def 4;
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 A62, JORDAN17:def 1;
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 A3, A4, A12, JGRAPH_3:26, JORDAN6:57;
then A65: ( p3 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
LE p1,p3, rectangle ((- 1),1,(- 1),1) by A63, Th50, JORDAN6:58;
then A66: p3 = p2 by A63, A65, Th50, JORDAN6:57;
( f . p4 = f . p3 or f . p2 = f . p1 ) by A3, A5, A12, A64, JGRAPH_3:26, JORDAN6:57;
then ( p4 = p3 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
then ( p4 = p3 or p2,p3,p4,p1 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ) by A6, A62, A66, JORDAN17:12;
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 A3, A4, A12, JGRAPH_3:26, JORDAN6:57;
then A68: ( p3 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
( f . p4 = f . p3 or f . p2 = f . p1 ) by A3, A5, A12, A67, JGRAPH_3:26, JORDAN6:57;
then ( p4 = p3 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
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 A3, A5, A12, JGRAPH_3:26, JORDAN6:57;
then ( p4 = p3 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
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 A3, A4, A12, JGRAPH_3:26, JORDAN6:57;
then A71: ( p3 = p2 or p2 = p1 ) by A2, A11, FUNCT_1:def 4;
LE p1,p3, rectangle ((- 1),1,(- 1),1) by A69, Th50, JORDAN6:58;
then A72: p1 = p2 by A69, A71, Th50, JORDAN6:57;
( f . p4 = f . p3 or f . p2 = f . p3 ) by A4, A5, A12, A70, JGRAPH_3:26, JORDAN6:57;
then ( p4 = p3 or p2 = p3 ) by A2, A11, FUNCT_1:def 4;
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