let n be Nat; :: thesis: for Ne being Subset of NAT st Ne c= Segm n & n > 0 holds
min* Ne <= n - 1
let Ne be Subset of NAT; :: thesis: ( Ne c= Segm n & n > 0 implies min* Ne <= n - 1 )
assume that
A1: Ne c= Segm n and
A2: n > 0 ; :: thesis: min* Ne <= n - 1

now :: thesis: min* Ne <= n - 1

per cases ( not Ne is empty or Ne is empty ) ;

suppose not Ne is empty ; :: thesis: min* Ne <= n - 1

hence min* Ne <= n - 1 by A1, Th12; :: thesis: verum

end;

suppose Ne is empty ; :: thesis: min* Ne <= n - 1

then min* Ne = 0 by NAT_1:def 1;
hence min* Ne <= n - 1 by A2, NAT_1:20; :: thesis: verum

end;

end;

end;

hence min* Ne <= n - 1 ; :: thesis: verum