for u, v being non zero Element of (TOP-REAL 3)
for p, q being Element of (ProjectiveSpace (TOP-REAL 3)) st p <> q & p = Dir u & q = Dir v holds
not u <X> v is zero