theorem :: XXREAL_1:285

for r, s being ExtReal holds ].r,+infty.] \ [.s,+infty.] = ].r,s.[ by Th191, XXREAL_0:3;