let q, s be ExtReal; :: thesis: for r being Real st s < q holds
[.r,s.] c= ].-infty,q.[
let r be Real; :: thesis: ( s < q implies [.r,s.] c= ].-infty,q.[ )
r in REAL by XREAL_0:def 1;
then -infty < r by XXREAL_0:12;
hence ( s < q implies [.r,s.] c= ].-infty,q.[ ) by Th47; :: thesis: verum