( max (x,y) >= x & x >= min (x,y) ) by XXREAL_0:17, XXREAL_0:25;
hence max ((min (x,y)),(max (x,y))) = max (x,y) by XXREAL_0:def 10, XXREAL_0:2; :: thesis: verum