let N be non empty Subset of NAT; :: thesis: min N = min* N
A1: for n being ExtReal st n in N holds
min* N <= n by NAT_1:def 1;
min* N in N by NAT_1:def 1;
hence min N = min* N by A1, XXREAL_2:def 7; :: thesis: verum