let n be Nat; :: thesis: n ! >= 1
n ! >= 0 + 1 by NAT_1:13;
hence n ! >= 1 ; :: thesis: verum