let s be ExtReal; :: thesis: for p being Real holds [.-infty,+infty.[ \ ].p,s.] = [.-infty,p.] \/ ].s,+infty.[
let p be Real; :: thesis: [.-infty,+infty.[ \ ].p,s.] = [.-infty,p.] \/ ].s,+infty.[
p in REAL by XREAL_0:def 1;
hence [.-infty,+infty.[ \ ].p,s.] = [.-infty,p.] \/ ].s,+infty.[ by Th329, XXREAL_0:9; :: thesis: verum