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

proof

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;

hence [.b,a.] is Element of Ext_Borel_Sets by CrossTh; :: thesis: verum