theorem Th10: :: BKMODEL3:9

for a, b, c being Real st a * (- b) = c & a * c = b holds
( c = 0 & b = 0 )