let p, q be Real; :: thesis: ].p,q.[ is open
defpred S1[ Real] means ( $1 <= p or q <= $1 );
consider X being Subset of REAL such that
A1: for r being Element of REAL holds
( r in X iff S1[r] ) from SUBSET_1:sch 3();
now :: thesis: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent holds
lim s1 in X
let s1 be Real_Sequence; :: thesis: ( rng s1 c= X & s1 is convergent implies lim s1 in X )
assume that
A2: rng s1 c= X and
A3: s1 is convergent ; :: thesis: lim s1 in X
A4: lim s1 in REAL by XREAL_0:def 1;
( lim s1 <= p or q <= lim s1 )
proof
assume A5: ( not lim s1 <= p & not q <= lim s1 ) ; :: thesis: contradiction
then 0 < (lim s1) - p by XREAL_1:50;
then consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
|.((s1 . m) - (lim s1)).| < (lim s1) - p by A3, SEQ_2:def 7;
0 < q - (lim s1) by A5, XREAL_1:50;
then consider n being Nat such that
A7: for m being Nat st n <= m holds
|.((s1 . m) - (lim s1)).| < q - (lim s1) by A3, SEQ_2:def 7;
consider k being Nat such that
A8: max (n,n1) < k by SEQ_4:3;
n1 <= max (n,n1) by XXREAL_0:25;
then n1 <= k by A8, XXREAL_0:2;
then A9: |.((s1 . k) - (lim s1)).| < (lim s1) - p by A6;
- |.((s1 . k) - (lim s1)).| <= (s1 . k) - (lim s1) by ABSVALUE:4;
then - ((s1 . k) - (lim s1)) <= - (- |.((s1 . k) - (lim s1)).|) by XREAL_1:24;
then - ((s1 . k) - (lim s1)) < (lim s1) - p by A9, XXREAL_0:2;
then - ((lim s1) - p) < - (- ((s1 . k) - (lim s1))) by XREAL_1:24;
then p - (lim s1) < (s1 . k) - (lim s1) ;
then A10: p < s1 . k by XREAL_1:9;
n <= max (n,n1) by XXREAL_0:25;
then n <= k by A8, XXREAL_0:2;
then ( (s1 . k) - (lim s1) <= |.((s1 . k) - (lim s1)).| & |.((s1 . k) - (lim s1)).| < q - (lim s1) ) by A7, ABSVALUE:4;
then (s1 . k) - (lim s1) < q - (lim s1) by XXREAL_0:2;
then A11: s1 . k < q by XREAL_1:9;
A12: k in NAT by ORDINAL1:def 12;
A13: s1 . k in REAL by XREAL_0:def 1;
dom s1 = NAT by FUNCT_2:def 1;
then s1 . k in rng s1 by FUNCT_1:def 3, A12;
hence contradiction by A1, A2, A11, A10, A13; :: thesis: verum
end;
hence lim s1 in X by A1, A4; :: thesis: verum
end;
then A14: X is closed ;
now :: thesis: for r being Real st r in ].p,q.[ ` holds
r in X
let r be Real; :: thesis: ( r in ].p,q.[ ` implies r in X )
A15: r in REAL by XREAL_0:def 1;
assume r in ].p,q.[ ` ; :: thesis: r in X
then not r in ].p,q.[ by XBOOLE_0:def 5;
then ( r <= p or q <= r ) ;
hence r in X by A1, A15; :: thesis: verum
end;
then A16: ].p,q.[ ` c= X ;
now :: thesis: for r being Real st r in X holds
r in ].p,q.[ `
let r be Real; :: thesis: ( r in X implies r in ].p,q.[ ` )
assume r in X ; :: thesis: r in ].p,q.[ `
then for s being Real holds
( not s = r or not p < s or not s < q ) by A1;
then ( r in REAL & not r in ].p,q.[ ) by XREAL_0:def 1;
hence r in ].p,q.[ ` by XBOOLE_0:def 5; :: thesis: verum
end;
then X c= ].p,q.[ ` ;
then ].p,q.[ ` = X by A16;
hence ].p,q.[ is open by A14; :: thesis: verum