:: deftheorem defines Lmi_sigmaFIELD MEASURE7:def 12 :
Lmi_sigmaFIELD = sigma_Field OS_Meas;