theorem :: BORSUK_5:25

for r being irrational Real holds frac r is irrational ;