theorem Th25: :: ANPROJ11:25

for P being non zero_proj2 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_proj2 P holds
|{(dir2a P),(dir2b P),v}| = - |(u,v)|