theorem :: STIRL2_1:4

for Ke, Ne being Subset of NAT st not min* Ne in Ne /\ Ke holds
min* Ne = min* (Ne \ Ke)