let q, s be ext-real number ; :: thesis: [.-infty ,q.] \ ].-infty ,s.] = {-infty } \/ ].s,q.]
( -infty <= s & -infty <= q ) by XXREAL_0:5;
hence [.-infty ,q.] \ ].-infty ,s.] = {-infty } \/ ].s,q.] by Th324; :: thesis: verum