theorem :: STIRL2_1:13

for n being Nat
for N being non empty Subset of NAT st N c= Segm n & N <> {(n - 1)} holds
min* N < n - 1