let s be ExtReal; for p being Real holds [.-infty,+infty.[ \ ].p,s.[ = [.-infty,p.] \/ [.s,+infty.[
let p be Real; [.-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; verum