:: deftheorem defines B-Meas MEASUR12:def 10 :
B-Meas = (sigma_Meas (C_Meas J-Meas)) | Borel_Sets;