for P, Q being Element of absolute
for R being Element of real_projective_plane
for u, v, w being non zero Element of (TOP-REAL 3) st P = Dir u & Q = Dir v & R = Dir w & R in tangent P & R in tangent Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 0 & not P = Q holds
( u . 1 = - (v . 1) & u . 2 = - (v . 2) )