theorem Th8: :: QMAX_1:9

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