A1: now

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

end;

now

assume r is not Integer ; :: thesis: ( r <= [\r/] + 1 & [\r/] + 1 < r + 1 )
then [\r/] < r by Th48;
hence ( r <= [\r/] + 1 & [\r/] + 1 < r + 1 ) by Th52, XREAL_1:6; :: thesis: verum

end;

hence ex b₁ being Integer st
( r <= b₁ & b₁ < r + 1 ) by A1; :: thesis: verum