let r, s be ExtReal; :: thesis: for p being Real st r < s holds
].r,+infty.[ \ ].p,s.] = ].r,p.] \/ ].s,+infty.[
let p be Real; :: thesis: ( 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; :: thesis: verum