theorem Th6: :: UNIROOTS:6
for q being Real st q > 0 holds
for r being Element of F_Complex st |.r.| = 1 & r <> [**1,0**] holds
|.([**q,0**] - r).| > q - 1