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