:: deftheorem Def12 defines PropRel QMAX_1:def 12 :
for Q being Quantum_Mechanics
for b₂ being Equivalence_Relation of (Prop Q) holds
( b₂ = PropRel Q iff for p, q being Element of Prop Q holds
( [p,q] in b₂ iff p <==> q ) );