theorem :: XXREAL_1:377

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