let Ne, Ke 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

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 ( min* (Ne \ Ke) in Ne \ Ke & Ne \ Ke c= Ne ) by NAT_1:def 1, XBOOLE_1:36;
then ( min* (Ne \ Ke) <= min* Ne & min* Ne <= min* (Ne \ Ke) ) by A3, NAT_1:def 1;
hence min* Ne = min* (Ne \ Ke) by XXREAL_0:1; :: thesis: verum

end;

end;

end;

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