theorem Th71: :: JGRAPH_6:71

for p, q being Point of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ & p in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & q in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p `2 >= q `2 & p `2 < 0 holds
(f . p) `2 >= (f . q) `2