theorem Th70: :: JGRAPH_6:70

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)]|) holds
(f . p) `1 <= (f . q) `1