let S be non empty Subset of NAT ; :: thesis: ( 0 in S implies min S = 0 )
assume 0 in S ; :: thesis: min S = 0
then min S <= 0 by XXREAL_2:def 7;
hence min S = 0 by NAT_1:3; :: thesis: verum