theorem :: BORSUK_5:20

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