theorem Th16: :: BKMODEL4:26

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