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();
A2: ].p,q.[ ` = X

proof

thus ].p,q.[ ` c= X :: according to XBOOLE_0:def 10 :: thesis: X c= ].p,q.[ `

proof

now

let r be real number ; :: thesis: ( r in ].p,q.[ ` implies r in X )
assume A3: r in ].p,q.[ ` ; :: thesis: r in X
A4: r is Real by XREAL_0:def 1;
not r in ].p,q.[ by A3, XBOOLE_0:def 5;
then ( r <= p or q <= r ) by A4;
hence r in X by A1, A4; :: thesis: verum

end;

hence ].p,q.[ ` c= X by MEMBERED:def 9; :: thesis: verum

end;

now

let r be real number ; :: thesis: ( r in X implies r in ].p,q.[ ` )
assume A5: r in X ; :: thesis: r in ].p,q.[ `
A6: r is Real by XREAL_0:def 1;
for s being Real holds
( not s = r or not p < s or not s < q ) by A1, A5;
then not r in ].p,q.[ ;
hence r in ].p,q.[ ` by A6, XBOOLE_0:def 5; :: thesis: verum

end;

hence X c= ].p,q.[ ` by MEMBERED:def 9; :: thesis: verum

end;

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= X & s1 is convergent implies lim s1 in X )
assume A7: ( rng s1 c= X & s1 is convergent ) ; :: thesis: lim s1 in X
( lim s1 <= p or q <= lim s1 )

proof

assume A8: ( not lim s1 <= p & not q <= lim s1 ) ; :: thesis: contradiction
then A9: 0 < (lim s1) - p by XREAL_1:52;
0 < q - (lim s1) by A8, XREAL_1:52;
then consider n being Element of NAT such that
A10: for m being Element of NAT st n <= m holds
abs ((s1 . m) - (lim s1)) < q - (lim s1) by A7, SEQ_2:def 7;
consider n1 being Element of NAT such that
A11: for m being Element of NAT st n1 <= m holds
abs ((s1 . m) - (lim s1)) < (lim s1) - p by A7, A9, SEQ_2:def 7;
consider k being Element of NAT such that
A12: max n,n1 < k by SEQ_4:10;
A13: ( - (abs ((s1 . k) - (lim s1))) <= (s1 . k) - (lim s1) & (s1 . k) - (lim s1) <= abs ((s1 . k) - (lim s1)) ) by ABSVALUE:11;
then A14: - ((s1 . k) - (lim s1)) <= - (- (abs ((s1 . k) - (lim s1)))) by XREAL_1:26;
n <= max n,n1 by XXREAL_0:25;
then n <= k by A12, XXREAL_0:2;
then abs ((s1 . k) - (lim s1)) < q - (lim s1) by A10;
then (s1 . k) - (lim s1) < q - (lim s1) by A13, XXREAL_0:2;
then A15: s1 . k < q by XREAL_1:11;
n1 <= max n,n1 by XXREAL_0:25;
then n1 <= k by A12, XXREAL_0:2;
then abs ((s1 . k) - (lim s1)) < (lim s1) - p by A11;
then - ((s1 . k) - (lim s1)) < (lim s1) - p by A14, XXREAL_0:2;
then - ((lim s1) - p) < - (- ((s1 . k) - (lim s1))) by XREAL_1:26;
then p - (lim s1) < (s1 . k) - (lim s1) ;
then A16: p < s1 . k by XREAL_1:11;
dom s1 = NAT by FUNCT_2:def 1;
then s1 . k in rng s1 by FUNCT_1:def 5;
hence contradiction by A1, A7, A15, A16; :: thesis: verum

end;

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

end;

then X is closed by Def4;
hence ].p,q.[ is open by A2, Def5; :: thesis: verum