let Ke, Ne be Subset of NAT; :: thesis: ( not min* Ne in Ne /\ Ke implies min* Ne = min* (Ne \ Ke) )
assume A1: not min* Ne in Ne /\ Ke ; :: thesis: min* Ne = min* (Ne \ Ke)

now :: thesis: min* Ne = min* (Ne \ Ke)

per cases ( Ne is empty or not Ne is empty ) ;

suppose Ne is empty ; :: thesis: min* Ne = min* (Ne \ Ke)

hence min* Ne = min* (Ne \ Ke) ; :: thesis: verum

end;

suppose not Ne is empty ; :: thesis: min* Ne = min* (Ne \ Ke)

then A2: min* Ne in Ne by NAT_1:def 1;
then not min* Ne in Ke by A1, XBOOLE_0:def 4;
then A3: min* Ne in Ne \ Ke by A2, XBOOLE_0:def 5;
then A4: min* (Ne \ Ke) <= min* Ne by NAT_1:def 1;
A5: Ne \ Ke c= Ne by XBOOLE_1:36;
min* (Ne \ Ke) in Ne \ Ke by A3, NAT_1:def 1;
then min* Ne <= min* (Ne \ Ke) by A5, NAT_1:def 1;
hence min* Ne = min* (Ne \ Ke) by A4, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence min* Ne = min* (Ne \ Ke) ; :: thesis: verum