let K, N be non empty Subset of NAT ; :: thesis: min (min K),(min N) = min (K \/ N)
set m = min (min N),(min K);
A1: for k being ext-real number st k in N \/ K holds
min (min N),(min K) <= k

proof

let k be ext-real number ; :: thesis: ( k in N \/ K implies min (min N),(min K) <= k )
assume k in N \/ K ; :: thesis: min (min N),(min K) <= k
then ( k in N or k in K ) by XBOOLE_0:def 3;
then A2: ( min N <= k or min K <= k ) by XXREAL_2:def 7;
A3: min (min N),(min K) <= min K by XXREAL_0:17;
min (min N),(min K) <= min N by XXREAL_0:17;
hence min (min N),(min K) <= k by A2, A3, XXREAL_0:2; :: thesis: verum

end;

( min (min N),(min K) = min N or min (min N),(min K) = min K ) by XXREAL_0:15;
then ( min (min N),(min K) in N or min (min N),(min K) in K ) by XXREAL_2:def 7;
then min (min N),(min K) in N \/ K by XBOOLE_0:def 3;
hence min (min K),(min N) = min (K \/ N) by A1, XXREAL_2:def 7; :: thesis: verum