let q, s be ExtReal; :: thesis: [.-infty,q.] \ ].-infty,s.[ = {-infty} \/ [.s,q.]
A1: -infty <= s by XXREAL_0:5;
-infty <= q by XXREAL_0:5;
hence [.-infty,q.] \ ].-infty,s.[ = {-infty} \/ [.s,q.] by A1, Th322; :: thesis: verum