:: deftheorem defines Borelsubsets_help FINANCE5:def 5 :
for r being Real
for I being TheEvent of r
for A being Element of Borel_Sets holds Borelsubsets_help (A,I) = A /\ I;