Family_of_Intervals c= sigma Family_of_Intervals by PROB_1:def 9;
then A1: Family_of_halflines c= sigma Family_of_Intervals by Th02;
now :: thesis: for x being object st x in Family_of_Intervals holds
x in Borel_Sets
let x be object ; :: thesis: ( x in Family_of_Intervals implies x in Borel_Sets )
assume x in Family_of_Intervals ; :: thesis: x in Borel_Sets
then ex I being Interval st x = I ;
hence x in Borel_Sets by Th03; :: thesis: verum
end;
then Family_of_Intervals c= Borel_Sets ;
hence sigma Family_of_Intervals = Borel_Sets by A1, PROB_1:def 9, PROB_1:def 12; :: thesis: sigma (Field_generated_by Family_of_Intervals) = Borel_Sets
hence sigma (Field_generated_by Family_of_Intervals) = Borel_Sets by SRINGS_3:23; :: thesis: verum