let a, b be Real; [.-infty,a.] /\ [.b,+infty.] = [.b,a.]
thus
[.-infty,a.] /\ [.b,+infty.] c= [.b,a.]
XBOOLE_0:def 10 [.b,a.] c= [.-infty,a.] /\ [.b,+infty.]proof
let x be
object ;
TARSKI:def 3 ( not x in [.-infty,a.] /\ [.b,+infty.] or x in [.b,a.] )
assume
x in [.-infty,a.] /\ [.b,+infty.]
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( not x in [.b,a.] or x in [.-infty,a.] /\ [.b,+infty.] )
assume
x in [.b,a.]
; 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; verum