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

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

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

( min ((min N),(min K)) = min N or min ((min N),(min K)) = min K )
by XXREAL_0:15;
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;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

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