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