for S being non empty Subset of NAT st 0 in S holds
min S = 0 by XXREAL_2:def 7;