:: deftheorem defines Borel_Sets PROB_1:def 12 :
Borel_Sets = sigma Family_of_halflines;