let a, b be Real; :: thesis: [.b,a.] is Element of Borel_Sets
Intersection (half_open_sets (b,a)) = [.b,a.] by Th6;
hence [.b,a.] is Element of Borel_Sets by Th5; :: thesis: verum