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