defpred S1[ 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 S1[i1] holds
- n <= i1
proof
let i1 be Integer; :: thesis: ( S1[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 S1[i0] ;
consider i1 being Integer such that
A5: ( S1[i1] & ( for i2 being Integer st S1[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 b1 being Integer st
( b1 <= r & r - 1 < b1 ) by A6, XREAL_1:146; :: thesis: verum