let N be non empty Subset of NAT ; :: thesis: min N = min* N
( min* N in N & ( for n being ext-real number st n in N holds
min* N <= n ) ) by NAT_1:def 1;
hence min N = min* N by XXREAL_2:def 7; :: thesis: verum