theorem Th2: :: ABIAN:2

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