:: deftheorem Def14 defines InvRel QMAX_1:def 14 :
for Q being Quantum_Mechanics
for b₂ being Function of (Class (PropRel Q)),(Class (PropRel Q)) holds
( b₂ = InvRel Q iff for p being Element of Prop Q holds b₂ . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) );