reconsider u = |[1,0,1]| 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_proj3 )
reconsider un = u as Element of REAL 3 by EUCLID:22;
( u . 1 <> 0 & u . 3 <> 0 ) ;
hence ( not P is zero_proj1 & not P is zero_proj3 ) ; :: thesis: verum