now :: thesis: for x, y being Element of {0,1,2} holds min (x,y) in {0,1,2}

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

end;

hence ( 2 in {0,1,2} & ( for x, y being Element of {0,1,2} holds min (x,y) in {0,1,2} ) ) by ENUMSET1:def 1; :: thesis: verum