:: deftheorem defines Meas QMAX_1:def 4 :
for Q being QM_Str
for A1 being Element of Obs Q
for s being Element of Sts Q holds Meas (A1,s) = the Quantum_Probability of Q . [A1,s];