:: deftheorem defines is_a_Quantum_Logic QMAX_1:def 7 :
for W being OrthoRelStr holds
( W is_a_Quantum_Logic iff ( the InternalRel of W partially_orders the carrier of W & the Compl of W is_an_involution & ( for x, y being Element of W st [x,y] in the InternalRel of W holds
[( the Compl of W . y),( the Compl of W . x)] in the InternalRel of W ) ) );