:: deftheorem defines frac INT_1:def 8 :
for r being Real holds frac r = r - [\r/];