let c be Nat; :: thesis: for b being positive Nat holds b divides (b + c) !
let b be positive Nat; :: thesis: b divides (b + c) !
b + c >= b + 0 by XREAL_1:6;
hence b divides (b + c) ! by NEWTON:41; :: thesis: verum