let a, b be Real; :: thesis: [.-infty,a.] /\ [.b,+infty.] = [.b,a.]
thus [.-infty,a.] /\ [.b,+infty.] c= [.b,a.] :: according to XBOOLE_0:def 10 :: thesis: [.b,a.] c= [.-infty,a.] /\ [.b,+infty.]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.-infty,a.] /\ [.b,+infty.] or x in [.b,a.] )
assume x in [.-infty,a.] /\ [.b,+infty.] ; :: thesis: x in [.b,a.]
then ( x in [.-infty,a.] & x in [.b,+infty.] ) by XBOOLE_0:def 4;
then B1: ( x in { c where c is Element of ExtREAL : ( -infty <= c & c <= a ) } & x in { c where c is Element of ExtREAL : ( b <= c & c <= +infty ) } ) by XXREAL_1:def 1;
consider c being Element of ExtREAL such that
B2: ( x = c & -infty <= c & c <= a ) by B1;
ex d being Element of ExtREAL st
( x = d & b <= d & d <= +infty ) by B1;
hence x in [.b,a.] by XXREAL_1:1, B2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.b,a.] or x in [.-infty,a.] /\ [.b,+infty.] )
assume x in [.b,a.] ; :: thesis: x in [.-infty,a.] /\ [.b,+infty.]
then x in { c where c is Element of ExtREAL : ( b <= c & c <= a ) } by XXREAL_1:def 1;
then consider c being Element of ExtREAL such that
B1: ( x = c & b <= c & c <= a ) ;
reconsider x = x as Element of ExtREAL by B1;
B2: ( -infty <= x & x <= +infty ) by XXREAL_0:3, XXREAL_0:5;
then F1: x in [.-infty,a.] by XXREAL_1:1, B1;
x in [.b,+infty.] by XXREAL_1:1, B2, B1;
hence x in [.-infty,a.] /\ [.b,+infty.] by XBOOLE_0:def 4, F1; :: thesis: verum