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; :: thesis: verum

end;

( r is not Integer implies ( r <= [\r/] + 1 & [\r/] + 1 < r + 1 ) ) by Th29, XREAL_1:6, Th26;
hence ex b₁ being Integer st
( r <= b₁ & b₁ < r + 1 ) by A1; :: thesis: verum