for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds dir3a P <> dir3b P by FINSEQ_1:78;