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