theorem :: BORSUK_5:19

for a being irrational Real holds - a is irrational ;