let n be non zero Nat; :: thesis: ( n - 1 is natural number & 1 <= n )
A1: 0 + 1 <= n by NAT_1:13;
then (0 + 1) - 1 <= n - 1 by XREAL_1:11;
then n - 1 in NAT by INT_1:16;
hence n - 1 is Nat ; :: thesis: 1 <= n
thus 1 <= n by A1; :: thesis: verum