:: deftheorem defines BorelSubsets FINANCE5:def 6 :
for r being Real
for I being TheEvent of r holds BorelSubsets I = { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ;