let r be Real; :: thesis: [\(frac r)/] = 0
[\(frac r)/] = [\(r + (- [\r/]))/]
.= [\r/] + (- [\r/]) by Th28
.= 0 ;
hence [\(frac r)/] = 0 ; :: thesis: verum