theorem Th42: :: ANPROJ11:42

for P being non zero_proj2 Element of (ProjectiveSpace (TOP-REAL 3)) holds not P in Line ((Pdir2a P),(Pdir2b P))