for u being non zero Element of (TOP-REAL 3)
for P being Element of absolute st P = Dir u & u . 3 = 1 holds
|[(u . 1),(u . 2)]| in circle (0,0,1)