theorem :: XXREAL_1:375

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