theorem :: XXREAL_1:385

for p, s being ExtReal holds REAL \ [.p,s.] = ].-infty,p.[ \/ ].s,+infty.[ by Th224, Th339, XXREAL_0:3;