let a, b be Real; :: thesis: max (a,b) >= min (a,b)

per cases ( min (a,b) = a or min (a,b) = b ) by XXREAL_0:15;

suppose min (a,b) = a ; :: thesis: max (a,b) >= min (a,b)

hence max (a,b) >= min (a,b) by XXREAL_0:25; :: thesis: verum

end;

suppose min (a,b) = b ; :: thesis: max (a,b) >= min (a,b)

hence max (a,b) >= min (a,b) by XXREAL_0:25; :: thesis: verum

end;

end;