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

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