let p be ext-real number ; :: thesis: for a being real number holds ].-infty ,p.[ /\ [.a,+infty .[ = [.a,p.[
let a be real number ; :: thesis: ].-infty ,p.[ /\ [.a,+infty .[ = [.a,p.[
a in REAL by XREAL_0:def 1;
then ( -infty < a & p <= +infty ) by XXREAL_0:3, XXREAL_0:12;
hence ].-infty ,p.[ /\ [.a,+infty .[ = [.a,p.[ by Th154; :: thesis: verum