theorem Th21: :: BORSUK_5:22

for a being Rational
for b being irrational Real st a <> 0 holds
a * b is irrational