theorem :: XXREAL_1:391

for r, s being ExtReal
for p being Real st r < s holds
].r,+infty.[ \ ].p,s.[ = ].r,p.] \/ [.s,+infty.[