let a, b be Real; :: thesis: ].-infty,a.] /\ [.b,+infty.[ = [.b,a.]
A1: a in REAL by XREAL_0:def 1;
b in REAL by XREAL_0:def 1;
then A2: -infty < b by XXREAL_0:12;
a < +infty by A1, XXREAL_0:9;
hence ].-infty,a.] /\ [.b,+infty.[ = [.b,a.] by A2, Th152; :: thesis: verum