for k1, k2 being Real holds [.k2,k1.[ is Element of Borel_Sets