let b be Real; :: thesis: [.b,+infty.] c= ].(b - 1),+infty.]
b - 1 < b by XREAL_1:44;
hence [.b,+infty.] c= ].(b - 1),+infty.] by XXREAL_1:39; :: thesis: verum