theorem Th56: :: BKMODEL1:67

for a being non zero Real
for u being Element of (TOP-REAL 3) st a * u = 0. (TOP-REAL 3) holds
u is zero