let r, s be ExtReal; for p being Real st r < s holds
].r,+infty.[ \ ].p,s.] = ].r,p.] \/ ].s,+infty.[
let p be Real; ( r < s implies ].r,+infty.[ \ ].p,s.] = ].r,p.] \/ ].s,+infty.[ )
p in REAL
by XREAL_0:def 1;
then
p < +infty
by XXREAL_0:9;
hence
( r < s implies ].r,+infty.[ \ ].p,s.] = ].r,p.] \/ ].s,+infty.[ )
by Th305; verum