theorem Th1: :: STIRL2_1:1

for N being non empty Subset of NAT holds min N = min* N