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