let s, g be Real; :: 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

set s2 = seq_const s;

A4: now :: thesis: for n being Nat holds (seq_const s) . n <= s1 . n

let n be Nat; :: thesis: (seq_const s) . n <= s1 . n
n in NAT by ORDINAL1:def 12;
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 (seq_const s) . n <= s1 . n by SEQ_1:57; :: thesis: verum

end;

(seq_const s) . 0 = s by SEQ_1:57;
then lim (seq_const s) = s by SEQ_4:25;
hence s <= lim s1 by A2, A4, SEQ_2:18; :: thesis: verum

end;

lim s1 <= g

proof

set s2 = seq_const g;

A5: now :: thesis: for n being Nat holds s1 . n <= (seq_const g) . n

let n be Nat; :: thesis: s1 . n <= (seq_const g) . n
n in NAT by ORDINAL1:def 12;
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 <= (seq_const g) . n by SEQ_1:57; :: thesis: verum

end;

(seq_const g) . 0 = g by SEQ_1:57;
then lim (seq_const g) = 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 ; :: thesis: verum