let Q be Quantum_Mechanics; :: thesis: for p, q being Element of Prop Q st p <==> q holds
q <==> p
let p, q be Element of Prop Q; :: thesis: ( p <==> q implies q <==> p )
assume ( p |- q & q |- p ) ; :: according to QMAX_1:def 11 :: thesis: q <==> p
hence q <==> p by Def11; :: thesis: verum