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

let x, y be Element of {0,1,2}; :: thesis: max (x,y) in {0,1,2}
( max (x,y) = x or max (x,y) = y ) by XXREAL_0:16;
hence max (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 max (x,y) in {0,1,2} ) ) by ENUMSET1:def 1; :: thesis: verum