let s, g be real number ; :: thesis: [.s,g.] is closed
for s1 being Real_Sequence st rng s1 c= [.s,g.] & s1 is convergent holds
lim s1 in [.s,g.]

proof

let s1 be Real_Sequence; :: thesis: ( rng s1 c= [.s,g.] & s1 is convergent implies lim s1 in [.s,g.] )
assume that
A1: rng s1 c= [.s,g.] and
A2: s1 is convergent ; :: thesis: lim s1 in [.s,g.]
A3: s <= lim s1

proof

s in REAL by XREAL_0:def 1;
then reconsider s2 = NAT --> s as Real_Sequence by FUNCOP_1:45;

A4: now

let n be Element of NAT ; :: thesis: s2 . n <= s1 . n
n in NAT ;
then n in dom s1 by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:def 3;
then s1 . n in [.s,g.] by A1;
then ex p being Real st
( s1 . n = p & s <= p & p <= g ) ;
hence s2 . n <= s1 . n by FUNCOP_1:7; :: thesis: verum

end;

s2 . 0 = s by FUNCOP_1:7;
then lim s2 = s by SEQ_4:25;
hence s <= lim s1 by A2, A4, SEQ_2:18; :: thesis: verum

end;

lim s1 <= g

proof

g in REAL by XREAL_0:def 1;
then reconsider s2 = NAT --> g as Real_Sequence by FUNCOP_1:45;

A5: now

let n be Element of NAT ; :: thesis: s1 . n <= s2 . n
n in NAT ;
then n in dom s1 by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:def 3;
then s1 . n in [.s,g.] by A1;
then ex p being Real st
( s1 . n = p & s <= p & p <= g ) ;
hence s1 . n <= s2 . n by FUNCOP_1:7; :: thesis: verum

end;

s2 . 0 = g by FUNCOP_1:7;
then lim s2 = g by SEQ_4:25;
hence lim s1 <= g by A2, A5, SEQ_2:18; :: thesis: verum

end;

hence lim s1 in [.s,g.] by A3; :: thesis: verum

end;

hence [.s,g.] is closed by Def4; :: thesis: verum