let n be Nat; :: thesis: for N being non empty Subset of NAT st N c= Segm n holds
min* N <= n - 1
let N be non empty Subset of NAT; :: thesis: ( N c= Segm n implies min* N <= n - 1 )
A1: min* N in N by NAT_1:def 1;
assume N c= Segm n ; :: thesis: min* N <= n - 1
hence min* N <= n - 1 by A1, Th10; :: thesis: verum