let A be Interval; :: thesis: A in Borel_Sets
A1: A in Family_of_Intervals by MEASUR10:def 1;
A2: Family_of_Intervals c= Field_generated_by Family_of_Intervals by SRINGS_3:21;
Field_generated_by Family_of_Intervals c= sigma (Field_generated_by Family_of_Intervals) by PROB_1:def 9;
hence A in Borel_Sets by A2, A1, MEASUR10:6; :: thesis: verum