theorem :: ANPROJ11:19

for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds dir1a P <> dir1b P by FINSEQ_1:78;