let
a
,
b
,
c
be
ExtReal
;
:: thesis:
(
a
in
REAL
&
a
<=
b
&
b
<
c
implies
b
in
REAL
)
assume
that
A1
: (
a
in
REAL
&
a
<=
b
)
and
A2
:
b
<
c
;
:: thesis:
b
in
REAL
(
b
in
REAL
or
b
=
+infty
)
by
A1
,
Th10
;
hence
b
in
REAL
by
A2
,
Lm9
;
:: thesis:
verum