now 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};
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}
;
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; verum