|[(u `1),(u `2)]| in circle (0,0,1) by A1, EUCLID:53;
then A2: |[(u . 1),(u `2)]| in circle (0,0,1) by EUCLID:def 9;
reconsider v = |[(u . 1),(u . 2),1]| as non zero Element of (TOP-REAL 3) by Th36;
reconsider P = Dir v as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
( v . 1 = v `1 & v . 2 = v `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;
then ( v . 1 = u . 1 & v . 2 = u . 2 ) by EUCLID_5:2;
then A3: |[(v . 1),(v . 2)]| in circle (0,0,1) by A2, EUCLID:def 10;
v . 3 = v `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ;
then P is Element of absolute by A3, Th69;
hence Dir |[(u . 1),(u . 2),1]| is Element of absolute ; :: thesis: verum