let r be Real; :: thesis: ( 0 < ([\r/] - r) + 1 & ([\r/] - r) + 1 <= 1 )
A1: r - r < ([\r/] + 1) - r by INT_1:29, XREAL_1:9;
[\r/] - r <= r - r by INT_1:def 6, XREAL_1:9;
then ([\r/] - r) + 1 <= (r - r) + 1 by XREAL_1:6;
hence ( 0 < ([\r/] - r) + 1 & ([\r/] - r) + 1 <= 1 ) by A1; :: thesis: verum