theorem :: QMAX_1:14

for Q being Quantum_Mechanics holds OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantum_Logic