theorem Th22: :: ANPROJ_9:26

for P being Point of (ProjectiveSpace (TOP-REAL 3)) ex a, b, c being Element of F_Real st
( P = Dir |[a,b,c]| & ( a <> 0 or b <> 0 or c <> 0 ) )