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 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 (); :: thesis: for f being Function of (),() 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 (),(); :: 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 Th50;
circle (0,0,1) = { p5 where p5 is Point of () : |.p5.| = 1 } by Th24;
then A4: P is being_simple_closed_curve by ;
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 :: thesis: ( ( LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) 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) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) 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) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) 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) & f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P ) )
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 ;
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, Th72; :: 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 ; :: 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 ; :: 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 ; :: 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 :: thesis: ( ( LE f . p1,f . p2,P & LE f . p2,f . p3,P & LE f . p3,f . p4,P & p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ) or ( LE f . p2,f . p3,P & LE f . p3,f . p4,P & LE f . p4,f . p1,P & p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ) or ( LE f . p3,f . p4,P & LE f . p4,f . p1,P & LE f . p1,f . p2,P & p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ) or ( LE f . p4,f . p1,P & LE f . p1,f . p2,P & LE f . p2,f . p3,P & p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ) )
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 ;
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)
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)
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)
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)
end;
end;
end;
hence p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ; :: thesis: verum
end;