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