for P being non zero_proj1 Element of (ProjectiveSpace (TOP-REAL 3)) holds not P in Line ((Pdir1a P),(Pdir1b P))