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