reconsider u = |[1,1,0]| as non zero Element of (TOP-REAL 3) ;
reconsider P = Dir u as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
take P ; :: thesis: ( not P is zero_proj1 & not P is zero_proj2 )
reconsider un = u as Element of REAL 3 by EUCLID:22;
|[1,1,0]| = |[(un . 1),(un . 2),(un . 3)]| by EUCLID_8:1;
then ( u . 1 <> 0 & u . 2 <> 0 ) by FINSEQ_1:78;
hence ( not P is zero_proj1 & not P is zero_proj2 ) ; :: thesis: verum