let s, g be Real; :: thesis:
let s1 be Real_Sequence; :: thesis:
assume A1: rng s1 c= [.s,g.] ; :: thesis:
thus s1 is bounded_above :: according to SEQ_2:def 8 :: thesis:

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

let t be Real; :: thesis:
assume t in rng s1 ; :: thesis:
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:

end;

let n be Nat; :: thesis:
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:

end;

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

let t be Real; :: thesis:
assume t in rng s1 ; :: thesis:
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:

end;

let n be Nat; :: thesis:
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: