let p1, p2, p3, p4 be Point of (TOP-REAL 2); 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); 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); ( 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
; ( 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 (TOP-REAL 2) : |.p5.| = 1 }
by Th24;
then A4:
P is being_simple_closed_curve
by A1, JGRAPH_3:26;
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 )
( 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)
;
f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P
now ( ( 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 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) )
;
f . p1,f . p2,f . p3,f . p4 are_in_this_order_on Pend; 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) )
;
f . p1,f . p2,f . p3,f . p4 are_in_this_order_on Pend; 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) )
;
f . p1,f . p2,f . p3,f . p4 are_in_this_order_on Pend; 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) )
;
f . p1,f . p2,f . p3,f . p4 are_in_this_order_on Pend;
hence
f . p1,
f . p2,
f . p3,
f . p4 are_in_this_order_on P
;
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) )
verumproof
assume A6:
f . p1,
f . p2,
f . p3,
f . p4 are_in_this_order_on P
;
p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1)
now ( ( 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 A6, JORDAN17:def 1;
case
(
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)end; case
(
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)then
p2,
p3,
p4,
p1 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1)
by A1, A2, Th77;
hence
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1)
by A3, JORDAN17:12;
verum end; case
(
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)then
p3,
p4,
p1,
p2 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1)
by A1, A2, Th77;
hence
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1)
by A3, JORDAN17:11;
verum end; case
(
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)then
p4,
p1,
p2,
p3 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1)
by A1, A2, Th77;
hence
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1)
by A3, JORDAN17:10;
verum end;
hence
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1)
;
verum
end;