theorem Th43: :: ANPROJ11:43

for P being non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)) holds not P in Line ((Pdir3a P),(Pdir3b P))