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.[
q in REAL by XREAL_0:def 1;
then ( -infty <= s & -infty < q ) by XXREAL_0:5, XXREAL_0:12;
hence [.-infty ,q.[ \ ].-infty ,s.] = {-infty } \/ ].s,q.[ by Th323; :: thesis: verum