let
a
,
b
be
ExtReal
;
:: thesis:
(
a
<=
min
(
a
,
b
) implies
min
(
a
,
b
)
=
a
)
assume
min
(
a
,
b
)
>=
a
;
:: thesis:
min
(
a
,
b
)
=
a
then
(
min
(
a
,
b
)
>
a
or
min
(
a
,
b
)
=
a
)
by
Th1
;
hence
min
(
a
,
b
)
=
a
by
Th17
;
:: thesis:
verum