for L being LINE of (IncProjSp_of real_projective_plane)
for P, Q being Element of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3) st P in L & Q in L & P = Dir u & Q = Dir v & u `3 <> 0 & v `3 = 0 holds
( P <> Q & Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L )