theorem Th28: :: ANPROJ11:28

for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds Dir (dir3a P) <> Dir (dir3b P)