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 Th297; :: thesis: verum