for Q being Quantum_Mechanics
for p, q being Element of Prop Q st p |- q holds
'not' q |- 'not' p