:: deftheorem defines L_mi MEASURE7:def 13 :
L_mi = sigma_Meas OS_Meas;