let s, g be real number ; :: 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 Element of NAT holds not r <= s1 . b₁
A2: for t being real number st t in rng s1 holds
t < r

proof

let t be real number ; :: 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;

for n being Element of NAT holds s1 . n < r

proof

let n be Element of NAT ; :: thesis: s1 . n < r
n in NAT ;
then n in dom s1 by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:def 3;
hence s1 . n < r by A2; :: thesis: verum

end;

hence for b₁ being Element of NAT holds not r <= s1 . b₁ ; :: thesis: verum

end;

thus s1 is bounded_below :: thesis: verum

proof

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

proof

let t be real number ; :: 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;

for n being Element of NAT holds r < s1 . n

proof

let n be Element of NAT ; :: thesis: r < 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;
hence r < s1 . n by A5; :: thesis: verum

end;

hence for b₁ being Element of NAT holds not s1 . b₁ <= r ; :: thesis: verum

end;