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, Th321, XXREAL_0:12; :: thesis: verum