assume
[.
r
,
s
.[
is
right_end
;
:: thesis:
contradiction
then
A3
:
sup
[.
r
,
s
.[
in
[.
r
,
s
.[
;
then
A4
:
sup
[.
r
,
s
.[
<
s
by
XXREAL_1:3
;
r
<=
sup
[.
r
,
s
.[
by
A3
,
XXREAL_1:3
;
then
r
<
s
by
A4
,
XXREAL_0:2
;
then
s
=
sup
[.
r
,
s
.[
by
Th31
;
hence
contradiction
by
A3
,
XXREAL_1:3
;
:: thesis:
verum