assume
].
r
,
s
.]
is
left_end
;
:: thesis:
contradiction
then
A1
:
inf
].
r
,
s
.]
in
].
r
,
s
.]
;
then
A2
:
inf
].
r
,
s
.]
<=
s
by
XXREAL_1:2
;
r
<
inf
].
r
,
s
.]
by
A1
,
XXREAL_1:2
;
then
r
<
s
by
A2
,
XXREAL_0:2
;
then
r
=
inf
].
r
,
s
.]
by
Th27
;
hence
contradiction
by
A1
,
XXREAL_1:2
;
:: thesis:
verum