let
a
,
b
,
c
be
ExtReal
;
:: thesis:
(
a
<
b
&
b
<
c
implies
b
in
REAL
)
assume
A1
: (
a
<
b
&
b
<
c
) ;
:: thesis:
b
in
REAL
(
b
in
REAL
or
b
=
+infty
or
b
=
-infty
)
by
Lm10
;
hence
b
in
REAL
by
A1
,
Lm8
,
Lm9
;
:: thesis:
verum