let r be Real; :: thesis: for n being Nat holds
( r - (1 / (n + 1)) < r & r < r + (1 / (n + 1)) )
let n be Nat; :: thesis: ( r - (1 / (n + 1)) < r & r < r + (1 / (n + 1)) )
0 < 1 / (n + 1) by XREAL_1:139;
hence ( r - (1 / (n + 1)) < r & r < r + (1 / (n + 1)) ) by Lm1; :: thesis: verum