let b be Nat; :: thesis: (b + 1) ! >= 2 |^ b

per cases ( b >= 2 or b = 0 or b = 1 ) by NAT_1:23;

suppose b >= 2 ; :: thesis: (b + 1) ! >= 2 |^ b

hence (b + 1) ! >= 2 |^ b by Th22; :: thesis: verum

end;

suppose b = 0 ; :: thesis: (b + 1) ! >= 2 |^ b

hence (b + 1) ! >= 2 |^ b by NEWTON:4, NEWTON:13; :: thesis: verum

end;

suppose b = 1 ; :: thesis: (b + 1) ! >= 2 |^ b

hence (b + 1) ! >= 2 |^ b by NEWTON:14; :: thesis: verum

end;

end;