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 & q <==> q ) by Th23;
then ( [p,p] in PropRel Q & [q,q] in PropRel Q ) by Def12;
then A1: ( p in Class (PropRel Q),p & q in Class (PropRel Q),q ) by EQREL_1:27;
A2: ( Class (PropRel Q),p in Class (PropRel Q) & Class (PropRel Q),q in Class (PropRel Q) ) by EQREL_1:def 5;
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, Th30;
hence [(Class (PropRel Q),p),(Class (PropRel Q),q)] in OrdRel Q by A2, Def13; :: thesis: verum

end;

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