theorem Th26: :: BKMODEL3:31

for a, b, c, d being Real
for u, v being non zero Element of (TOP-REAL 3) st u = |[a,b,1]| & v = |[c,d,0]| holds
Dir u <> Dir v