let
a
,
b
be
ExtReal
;
:: thesis:
min
(
a
,
b
)
<=
a
(
a
<=
b
or not
a
<=
b
) ;
hence
min
(
a
,
b
)
<=
a
by
Def8
;
:: thesis:
verum