A1: now :: thesis: ( r is Integer implies ( r <= [\r/] & [\r/] < r + 1 ) )
A2: r + 0 < r + 1 by XREAL_1:6;
assume r is Integer ; :: thesis: ( r <= [\r/] & [\r/] < r + 1 )
hence ( r <= [\r/] & [\r/] < r + 1 ) by A2, Th25; :: thesis: verum
end;
( r is not Integer implies ( r <= [\r/] + 1 & [\r/] + 1 < r + 1 ) ) by Th29, XREAL_1:6, Th26;
hence ex b1 being Integer st
( r <= b1 & b1 < r + 1 ) by A1; :: thesis: verum