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