theorem Th1: :: JGRAPH_5:1
for p being Point of (TOP-REAL 2) st |.p.| <= 1 holds
( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 )