let p, q be real number ; :: thesis: ].p,q.[ is open
defpred S₁[ Real] means ( $1 <= p or q <= $1 );
consider X being Subset of REAL such that
A1: for r being Real holds
( r in X iff S₁[r] ) from SUBSET_1:sch 3();

now

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
( lim s1 <= p or q <= lim s1 )

proof

assume A4: ( not lim s1 <= p & not q <= lim s1 ) ; :: thesis: contradiction
then 0 < (lim s1) - p by XREAL_1:50;
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
abs ((s1 . m) - (lim s1)) < (lim s1) - p by A3, SEQ_2:def 7;
0 < q - (lim s1) by A4, XREAL_1:50;
then consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds
abs ((s1 . m) - (lim s1)) < q - (lim s1) by A3, SEQ_2:def 7;
consider k being Element of NAT such that
A7: max (n,n1) < k by SEQ_4:3;
n1 <= max (n,n1) by XXREAL_0:25;
then n1 <= k by A7, XXREAL_0:2;
then A8: abs ((s1 . k) - (lim s1)) < (lim s1) - p by A5;
- (abs ((s1 . k) - (lim s1))) <= (s1 . k) - (lim s1) by ABSVALUE:4;
then - ((s1 . k) - (lim s1)) <= - (- (abs ((s1 . k) - (lim s1)))) by XREAL_1:24;
then - ((s1 . k) - (lim s1)) < (lim s1) - p by A8, XXREAL_0:2;
then - ((lim s1) - p) < - (- ((s1 . k) - (lim s1))) by XREAL_1:24;
then p - (lim s1) < (s1 . k) - (lim s1) ;
then A9: p < s1 . k by XREAL_1:9;
n <= max (n,n1) by XXREAL_0:25;
then n <= k by A7, XXREAL_0:2;
then ( (s1 . k) - (lim s1) <= abs ((s1 . k) - (lim s1)) & abs ((s1 . k) - (lim s1)) < q - (lim s1) ) by A6, ABSVALUE:4;
then (s1 . k) - (lim s1) < q - (lim s1) by XXREAL_0:2;
then A10: s1 . k < q by XREAL_1:9;
dom s1 = NAT by FUNCT_2:def 1;
then s1 . k in rng s1 by FUNCT_1:def 3;
hence contradiction by A1, A2, A10, A9; :: thesis: verum

end;

hence lim s1 in X by A1; :: thesis: verum

end;

then A11: X is closed by Def4;

now

let r be real number ; :: thesis: ( r in ].p,q.[ ` implies r in X )
A12: r is 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 ) by A12;
hence r in X by A1, A12; :: thesis: verum

end;

then A13: ].p,q.[ ` c= X by MEMBERED:def 9;

now

let r be real number ; :: 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 is 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.[ ` by MEMBERED:def 9;
then ].p,q.[ ` = X by A13, XBOOLE_0:def 10;
hence ].p,q.[ is open by A11, Def5; :: thesis: verum