for n being Nat
for N being non empty Subset of NAT st N c= n holds
n - 1 is Element of NAT