theorem Th22: :: BORSUK_5:23

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