let Ke, Ne be Subset of NAT; :: thesis: min ((min* Ke),(min* Ne)) <= min* (Ke \/ Ne)

now :: thesis: min ((min* Ke),(min* Ne)) <= min* (Ke \/ Ne)

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

suppose ( Ke is empty or Ne is empty ) ; :: thesis: min ((min* Ke),(min* Ne)) <= min* (Ke \/ Ne)

then ( ( min* Ke = 0 & min* Ne >= 0 ) or ( min* Ne = 0 & min* Ke >= 0 ) ) by NAT_1:def 1;
hence min ((min* Ke),(min* Ne)) <= min* (Ke \/ Ne) by XXREAL_0:def 9; :: thesis: verum

end;

suppose ( not Ke is empty & not Ne is empty ) ; :: thesis: min ((min* Ke),(min* Ne)) <= min* (Ke \/ Ne)

then reconsider K = Ke, N = Ne as non empty Subset of NAT ;
A1: min N = min* Ne by Th1;
A2: min (K \/ N) = min* (Ke \/ Ne) by Th1;
min K = min* Ke by Th1;
hence min ((min* Ke),(min* Ne)) <= min* (Ke \/ Ne) by A1, A2, Th2; :: thesis: verum

end;

end;

end;

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