theorem Th14: :: STIRL2_1:14

for n being Nat
for Ne being Subset of NAT st Ne c= Segm n & n > 0 holds
min* Ne <= n - 1