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