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

end;

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