theorem :: XXREAL_1:284

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