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

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