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