theorem Th72:
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 &
LE p1,
p2,
rectangle (
(- 1),1,
(- 1),1) &
LE p2,
p3,
rectangle (
(- 1),1,
(- 1),1) &
LE p3,
p4,
rectangle (
(- 1),1,
(- 1),1) holds
f . p1,
f . p2,
f . p3,
f . p4 are_in_this_order_on P