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 holds
( p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 iff f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P )
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 holds
( p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 iff f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P )
let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( P = circle 0 ,0 ,1 & f = Sq_Circ implies ( p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 iff 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: ( p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 iff 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 Th60;
circle 0 ,0 ,1 = { p5 where p5 is Point of (TOP-REAL 2) : |.p5.| = 1 } by Th33;
then A4: P is being_simple_closed_curve by A1, JGRAPH_3:36;
thus ( p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 implies f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) :: thesis: ( f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P implies p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 )
proof
assume A5: p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
now
per cases ( ( LE p1,p2, rectangle (- 1),1,(- 1),1 & LE p2,p3, rectangle (- 1),1,(- 1),1 & LE p3,p4, rectangle (- 1),1,(- 1),1 ) or ( LE p2,p3, rectangle (- 1),1,(- 1),1 & LE p3,p4, rectangle (- 1),1,(- 1),1 & LE p4,p1, rectangle (- 1),1,(- 1),1 ) or ( LE p3,p4, rectangle (- 1),1,(- 1),1 & LE p4,p1, rectangle (- 1),1,(- 1),1 & LE p1,p2, rectangle (- 1),1,(- 1),1 ) or ( LE p4,p1, rectangle (- 1),1,(- 1),1 & LE p1,p2, rectangle (- 1),1,(- 1),1 & LE p2,p3, rectangle (- 1),1,(- 1),1 ) ) by A5, JORDAN17:def 1;
case ( LE p1,p2, rectangle (- 1),1,(- 1),1 & LE p2,p3, rectangle (- 1),1,(- 1),1 & LE p3,p4, rectangle (- 1),1,(- 1),1 ) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A1, A2, Th82; :: thesis: verum
end;
case ( LE p2,p3, rectangle (- 1),1,(- 1),1 & LE p3,p4, rectangle (- 1),1,(- 1),1 & LE p4,p1, rectangle (- 1),1,(- 1),1 ) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A1, A2, A4, Th82, JORDAN17:12; :: thesis: verum
end;
case ( LE p3,p4, rectangle (- 1),1,(- 1),1 & LE p4,p1, rectangle (- 1),1,(- 1),1 & LE p1,p2, rectangle (- 1),1,(- 1),1 ) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A1, A2, A4, Th82, JORDAN17:11; :: thesis: verum
end;
case ( LE p4,p1, rectangle (- 1),1,(- 1),1 & LE p1,p2, rectangle (- 1),1,(- 1),1 & LE p2,p3, rectangle (- 1),1,(- 1),1 ) ; :: thesis: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P by A1, A2, A4, Th82, JORDAN17:10; :: thesis: verum
end;
end;
end;
hence f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis: verum
end;
thus ( f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P implies p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 ) :: thesis: verum
proof
assume A6: f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ; :: thesis: p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1
now
per cases ( ( LE f . p1,f . p2,P & LE f . p2,f . p3,P & LE f . p3,f . p4,P ) or ( LE f . p2,f . p3,P & LE f . p3,f . p4,P & LE f . p4,f . p1,P ) or ( LE f . p3,f . p4,P & LE f . p4,f . p1,P & LE f . p1,f . p2,P ) or ( LE f . p4,f . p1,P & LE f . p1,f . p2,P & LE f . p2,f . p3,P ) ) by A6, JORDAN17:def 1;
case ( LE f . p1,f . p2,P & LE f . p2,f . p3,P & LE f . p3,f . p4,P ) ; :: thesis: p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1
hence p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 by A1, A2, Th87; :: thesis: verum
end;
case ( LE f . p2,f . p3,P & LE f . p3,f . p4,P & LE f . p4,f . p1,P ) ; :: thesis: p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1
then p2,p3,p4,p1 are_in_this_order_on rectangle (- 1),1,(- 1),1 by A1, A2, Th87;
hence p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 by A3, JORDAN17:12; :: thesis: verum
end;
case ( LE f . p3,f . p4,P & LE f . p4,f . p1,P & LE f . p1,f . p2,P ) ; :: thesis: p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1
then p3,p4,p1,p2 are_in_this_order_on rectangle (- 1),1,(- 1),1 by A1, A2, Th87;
hence p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 by A3, JORDAN17:11; :: thesis: verum
end;
case ( LE f . p4,f . p1,P & LE f . p1,f . p2,P & LE f . p2,f . p3,P ) ; :: thesis: p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1
then p4,p1,p2,p3 are_in_this_order_on rectangle (- 1),1,(- 1),1 by A1, A2, Th87;
hence p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 by A3, JORDAN17:10; :: thesis: verum
end;
end;
end;
hence p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 ; :: thesis: verum
end;