theorem Th12: :: STIRL2_1:12

for n being Nat
for N being non empty Subset of NAT st N c= Segm n holds
min* N <= n - 1