let b be Nat; :: thesis: b ! <= b |^ b

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

suppose b >= 2 ; :: thesis: b ! <= b |^ b

hence b ! <= b |^ b by Th24; :: thesis: verum

end;

suppose b = 0 ; :: thesis: b ! <= b |^ b

hence b ! <= b |^ b by NEWTON:4, NEWTON:12; :: thesis: verum

end;

suppose b = 1 ; :: thesis: b ! <= b |^ b

hence b ! <= b |^ b by NEWTON:13; :: thesis: verum

end;

end;