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

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

end;

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