theorem Th66:
for
p1,
p2,
p3 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 &
p1 in LSeg (
|[(- 1),(- 1)]|,
|[(- 1),1]|) &
p1 `2 >= 0 &
LE p1,
p2,
rectangle (
(- 1),1,
(- 1),1) &
LE p2,
p3,
rectangle (
(- 1),1,
(- 1),1) holds
LE f . p2,
f . p3,
P