theorem Th37: :: BKMODEL1:43

for u, v being non zero Element of (TOP-REAL 3) st Dir u = Dir v & u . 3 = v . 3 & v . 3 <> 0 holds
u = v