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