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