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 ExtReal st k in N \/ K holds
min ((min N),(min K)) <= k

proof

let k be ExtReal; :: 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