theorem Th24: :: ANPROJ11:24

for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds Dir (dir2a P) <> Dir (dir2b P)