theorem Th68: :: JGRAPH_6:68

for p 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 f = Sq_Circ holds
( (f . p) `1 >= 0 iff p `1 >= 0 )