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