for P being non zero_proj1 Element of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3)
for v being Element of (TOP-REAL 3) st u = normalize_proj1 P holds
|{(dir1a P),(dir1b P),v}| = |(u,v)|