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