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