let a, b be real number ; :: 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;