defpred S₁[ Integer] means r < $1;
consider n being Nat such that
A1: - r < n by Lm7;
A2: - n < - (- r) by A1, XREAL_1:24;
A3: for i1 being Integer st S₁[i1] holds
- n <= i1

proof

let i1 be Integer; :: thesis: ( S₁[i1] implies - n <= i1 )
assume r < i1 ; :: thesis: - n <= i1
then r + (- n) < i1 + r by A2, XREAL_1:8;
hence - n <= i1 by XREAL_1:6; :: thesis: verum

end;

ex n being Nat st r < n by Lm7;
then A4: ex i0 being Integer st S₁[i0] ;
consider i1 being Integer such that
A5: ( S₁[i1] & ( for i2 being Integer st S₁[i2] holds
i1 <= i2 ) ) from INT_1:sch 5(A3, A4);
A6: r - 1 < i1 - 1 by A5, XREAL_1:9;
( r < i1 - 1 implies i1 <= i1 - 1 ) by A5;
hence ex b₁ being Integer st
( b₁ <= r & r - 1 < b₁ ) by A6, XREAL_1:146; :: thesis: verum