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

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

end;

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