:: deftheorem defines |- QMAX_1:def 10 :
for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p |- q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2) );