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: min (min N),(min K) <= min (N \/ K)

proof

( 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 A2: min (min N),(min K) in N \/ K by XBOOLE_0:def 3;
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 A3: k in N \/ K ; :: thesis: min (min N),(min K) <= k
( k in N or k in K ) by A3, XBOOLE_0:def 3;
then ( ( min N <= k or min K <= k ) & min (min N),(min K) <= min N & min (min N),(min K) <= min K ) by XXREAL_0:17, XXREAL_2:def 7;
hence min (min N),(min K) <= k by XXREAL_0:2; :: thesis: verum

end;

hence min (min N),(min K) <= min (N \/ K) by A2, XXREAL_2:def 7; :: thesis: verum

end;

min (N \/ K) <= min (min N),(min K)

proof

( min (N \/ K) <= min N & min (N \/ K) <= min K ) by XBOOLE_1:7, XXREAL_2:60;
hence min (N \/ K) <= min (min N),(min K) by XXREAL_0:20; :: thesis: verum

end;

hence min (min K),(min N) = min (K \/ N) by A1, XXREAL_0:1; :: thesis: verum