theorem Th23: :: BORSUK_5:24

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