let s be ext-real number ; :: thesis: for q being real number holds [.-infty ,q.[ \ ].-infty ,s.] = {-infty } \/ ].s,q.[
let q be real number ; :: thesis: [.-infty ,q.[ \ ].-infty ,s.] = {-infty } \/ ].s,q.[
A1: q in REAL by XREAL_0:def 1;
-infty <= s by XXREAL_0:5;
hence [.-infty ,q.[ \ ].-infty ,s.] = {-infty } \/ ].s,q.[ by A1, Th323, XXREAL_0:12; :: thesis: verum