let r, s be ext-real number ; :: thesis: for p being real number st r <= s holds
[.r,+infty.[ \ ].p,s.] = [.r,p.] \/ ].s,+infty.[
let p be real number ; :: thesis: ( r <= s implies [.r,+infty.[ \ ].p,s.] = [.r,p.] \/ ].s,+infty.[ )
p in REAL by XREAL_0:def 1;
hence ( r <= s implies [.r,+infty.[ \ ].p,s.] = [.r,p.] \/ ].s,+infty.[ ) by Th306, XXREAL_0:9; :: thesis: verum