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