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;