for P, Q, R being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3))
for u, v, w being non zero Element of (TOP-REAL 3) st P = Dir u & Q = Dir v & R = Dir w & u `3 = 1 & v `3 = 1 & w `3 = 1 holds
( P,Q,R are_collinear iff u,v,w are_collinear )