r in REAL by XREAL_0:def 1;
then reconsider b = NAT --> r as Real_Sequence by FUNCOP_1:45;
let a be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not rng a c= right_closed_halfline r or not a is convergent or lim a in right_closed_halfline r )
assume that
A1: rng a c= right_closed_halfline r and
A2: a is convergent ; :: thesis: lim a in right_closed_halfline r

A3: now

let n be Element of NAT ; :: thesis: b . n <= a . n
a . n in rng a by VALUED_0:28;
then a . n in right_closed_halfline r by A1;
then a . n in { g1 where g1 is Real : r <= g1 } by XXREAL_1:232;
then ex r1 being Real st
( a . n = r1 & r <= r1 ) ;
hence b . n <= a . n by FUNCOP_1:7; :: thesis: verum

end;

lim b = b . 0 by SEQ_4:26
.= r by FUNCOP_1:7 ;
then r <= lim a by A2, A3, SEQ_2:18;
then lim a in { g1 where g1 is Real : r <= g1 } ;
hence lim a in right_closed_halfline r by XXREAL_1:232; :: thesis: verum