let a, b be real number ; :: thesis: [.b,a.] is Element of Borel_Sets
Intersection (half_open_sets (b,a)) = [.b,a.] by SP2;
hence [.b,a.] is Element of Borel_Sets by BJ4; :: thesis: verum