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;
then p < +infty by XXREAL_0:9;
hence ( r <= s implies [.r,+infty .[ \ ].p,s.[ = [.r,p.] \/ [.s,+infty .[ ) by Th298; :: thesis: verum