let r be real irrational number ; :: thesis: frac r is irrational
frac r = r - [\r/] by INT_1:def 6;
hence frac r is irrational by Th41; :: thesis: verum