let Q be Quantum_Mechanics; :: thesis: for p, q being Element of Prop Q holds
( p |- q iff [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q )
let p, q be Element of Prop Q; :: thesis: ( p |- q iff [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q )
[p,p] in PropRel Q by Def12;
then A1: p in Class ((PropRel Q),p) by EQREL_1:19;
[q,q] in PropRel Q by Def12;
then A2: q in Class ((PropRel Q),q) by EQREL_1:19;
A3: ( Class ((PropRel Q),p) in Class (PropRel Q) & Class ((PropRel Q),q) in Class (PropRel Q) ) by EQREL_1:def 3;
thus ( p |- q implies [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q ) :: thesis: ( [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q implies p |- q )

proof

assume p |- q ; :: thesis: [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q
then for p1, q1 being Element of Prop Q st p1 in Class ((PropRel Q),p) & q1 in Class ((PropRel Q),q) holds
p1 |- q1 by A1, A2, A3, Th9;
hence [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q by A3, Def13; :: thesis: verum

end;

thus ( [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q implies p |- q ) by A1, A2, Def13; :: thesis: verum