theorem Th78:
for
p1,
p2,
p3,
p4 being
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 )