let a, b be Real; :: thesis: [.b,a.] is Element of Ext_Borel_Sets

B1: [.-infty,a.] is Element of Ext_Borel_Sets by Th3;

[.-infty,a.] /\ [.b,+infty.] is Element of Ext_Borel_Sets

B1: [.-infty,a.] is Element of Ext_Borel_Sets by Th3;

[.-infty,a.] /\ [.b,+infty.] is Element of Ext_Borel_Sets

proof

hence
[.b,a.] is Element of Ext_Borel_Sets
by CrossTh; :: thesis: verum
Intersection (ext_half_open_sets b) = [.b,+infty.]
by Th60;

then [.b,+infty.] is Element of Ext_Borel_Sets by Th50;

hence [.-infty,a.] /\ [.b,+infty.] is Element of Ext_Borel_Sets by B1, PROB_1:19; :: thesis: verum

end;then [.b,+infty.] is Element of Ext_Borel_Sets by Th50;

hence [.-infty,a.] /\ [.b,+infty.] is Element of Ext_Borel_Sets by B1, PROB_1:19; :: thesis: verum