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

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