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