let x, y be Element of {0,1,2}; :: thesis: min (x,y) in {0,1,2}
( min (x,y) = x or min (x,y) = y ) by XXREAL_0:15;
hence min (x,y) in {0,1,2} ; :: thesis: verum