theorem :: QMAX_1:6

for Q being Quantum_Mechanics
for p, q being Element of Prop Q st p <==> q holds
q <==> p ;