theorem :: XXREAL_1:292

for r being ExtReal
for s being Real holds ].r,+infty.] \ ].s,+infty.] = ].r,s.]