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