let s be ext-real number ; :: thesis: for p being real number holds [.-infty ,+infty .[ \ ].p,s.[ = [.-infty ,p.] \/ [.s,+infty .[
let p be real number ; :: 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 Th325, XXREAL_0:9; :: thesis: verum