for u, v being non zero Element of (TOP-REAL 3)
for k being non zero Real st u = k * v holds
Dir u = Dir v