for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds dir2a P <> dir2b P by FINSEQ_1:78;