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;
hence ( s <= q implies [.r,s.[ c= ].-infty,q.[ ) by Th48, XXREAL_0:12; :: thesis: verum