let seq be Real_Sequence; :: thesis:
assume that
A1: seq is non-increasing and
A2: seq is bounded_below ; :: thesis:
defpred S₁[ Real] means ex n being Element of NAT st c₁ = seq . n;
consider X being Subset of REAL such that
A3: for p being Real holds
( p in X iff S₁[p] ) from SUBSET_1:sch 3();
take g = lower_bound X; :: according to SEQ_2:def 6 :: thesis:
let s be real number ; :: thesis:
assume A4: 0 < s ; :: thesis:
A5: ( ex r being real number st
for p being real number st p in X holds
r <= p implies X is bounded_below )

given r being real number such that A6: for p being real number st p in X holds
r <= p ; :: thesis:
take r ; :: according to XXREAL_2:def 9 :: thesis:
let p be ext-real number ; :: according to XXREAL_2:def 2 :: thesis:
thus ( not p in X or r <= p ) by A6; :: thesis:

end;

seq . 0 in X by A3;
then consider p1 being real number such that
A7: p1 in X and
A8: p1 < (lower_bound X) + s by A5, A4, Def5;
consider n1 being Element of NAT such that
A9: p1 = seq . n1 by A3, A7;
take n = n1; :: thesis:
let m be Element of NAT ; :: thesis:
consider r1 being real number such that
A10: for n being Element of NAT holds r1 < seq . n by A2, SEQ_2:def 4;

A11: now

end;