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

Intersection (half_open_sets (b,a)) = [.b,a.] by Th6;

hence [.b,a.] is Element of Borel_Sets by Th5; :: thesis: verum