frac r = r - [\r/] by INT_1:def 8;
hence frac r is irrational ; :: thesis: verum