let b be Real; :: thesis: for n being Nat st n > 0 holds
[.b,+infty.] c= ].(b - (1 / n)),+infty.]
let n be Nat; :: thesis: ( n > 0 implies [.b,+infty.] c= ].(b - (1 / n)),+infty.] )
assume n > 0 ; :: thesis: [.b,+infty.] c= ].(b - (1 / n)),+infty.]
then b - (1 / n) < b by XREAL_1:44;
hence [.b,+infty.] c= ].(b - (1 / n)),+infty.] by XXREAL_1:39; :: thesis: verum