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;
( u . 1 <> 0 & u . 2 <> 0 ) ;
hence ( not P is zero_proj1 & not P is zero_proj2 ) ; :: thesis: verum