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, Th324; :: thesis: verum