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