:: deftheorem defines 'not' QMAX_1:def 9 :
for Q being Quantum_Mechanics
for p being Element of Prop Q holds 'not' p = [(p `1),((p `2) `)];