let
a
,
b
,
c
be
ExtReal
;
:: thesis:
(
a
<=
min
(
b
,
c
) implies
a
<=
b
)
min
(
b
,
c
)
<=
b
by
Th17
;
hence
(
a
<=
min
(
b
,
c
) implies
a
<=
b
)
by
Th2
;
:: thesis:
verum