let s, g be Real; :: thesis: for s1 being Real_Sequence st rng s1 c= [.s,g.] holds
s1 is bounded
let s1 be Real_Sequence; :: thesis: ( rng s1 c= [.s,g.] implies s1 is bounded )
assume A1: rng s1 c= [.s,g.] ; :: thesis: s1 is bounded
thus s1 is bounded_above :: according to SEQ_2:def 8 :: thesis: s1 is bounded_below

proof

take r = g + 1; :: according to SEQ_2:def 3 :: thesis: for b₁ being set holds not r <= s1 . b₁
A2: for t being Real st t in rng s1 holds
t < r

proof

let t be Real; :: thesis: ( t in rng s1 implies t < r )
assume t in rng s1 ; :: thesis: t < r
then t in [.s,g.] by A1;
then A3: ex p being Real st
( t = p & s <= p & p <= g ) ;
g < r by XREAL_1:29;
hence t < r by A3, XXREAL_0:2; :: thesis: verum

end;

let n be Nat; :: thesis: not r <= 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;
hence not r <= s1 . n by A2; :: thesis: verum

end;

take r = s - 1; :: according to SEQ_2:def 4 :: thesis: for b₁ being set holds not s1 . b₁ <= r
A4: r + 1 = s - (1 - 1) ;
A5: for t being Real st t in rng s1 holds
r < t

proof

let t be Real; :: thesis: ( t in rng s1 implies r < t )
assume t in rng s1 ; :: thesis: r < t
then t in [.s,g.] by A1;
then A6: ex p being Real st
( t = p & s <= p & p <= g ) ;
r < s by A4, XREAL_1:29;
hence r < t by A6, XXREAL_0:2; :: thesis: verum

end;

let n be Nat; :: thesis: not s1 . n <= r
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;
hence not s1 . n <= r by A5; :: thesis: verum