for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p |- q iff [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q )