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 )

( 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

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