:: deftheorem Def13 defines OrdRel QMAX_1:def 13 :
for Q being Quantum_Mechanics
for b₂ being Relation of (Class (PropRel Q)) holds
( b₂ = OrdRel Q iff for B, C being Subset of (Prop Q) holds
( [B,C] in b₂ iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) );