theorem :: BORSUK_5:21

for a being Rational
for b being irrational Real holds b - a is irrational ;