for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds Dir (dir1a P) <> Dir (dir1b P)