let n be Nat; :: thesis: for N being non empty Subset of NAT st N c= n holds
n - 1 is Element of NAT
let N be non empty Subset of NAT; :: thesis: ( N c= n implies n - 1 is Element of NAT )
A1: min* N in N by NAT_1:def 1;
assume N c= n ; :: thesis: n - 1 is Element of NAT
then min* N in n by A1;
then min* N in { l where l is Nat : l < n } by AXIOMS:4;
then ex l being Nat st
( min* N = l & l < n ) ;
hence n - 1 is Element of NAT by NAT_1:20; :: thesis: verum