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;