reconsider u = |[0,1,1]| as Element of (TOP-REAL 3) ;
not u is zero by EUCLID_5:4, FINSEQ_1:78;
hence Dir |[0,1,1]| is Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26; :: thesis: verum