let s be ExtReal; :: thesis: for q being Real holds [.-infty,q.[ \ ].-infty,s.[ = {-infty} \/ [.s,q.[
let q be Real; :: 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