let
seq
be
ExtREAL_sequence
;
:: thesis:
inf
seq
<=
sup
seq
A1
:
seq
.
0
<=
sup
seq
by
Th23
;
inf
seq
<=
seq
.
0
by
Th23
;
hence
inf
seq
<=
sup
seq
by
A1
,
XXREAL_0:2
;
:: thesis:
verum