theorem :: FINANCE2:6

for k1, k2 being Real holds ].k1,k2.] is Event of Borel_Sets