let Q be 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 )
let p, q be Element of Prop Q; ( 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 )
( [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q implies p |- q )proof
assume
p |- q
;
[(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;
verum
end;
thus
( [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q implies p |- q )
by A1, A2, Def13; verum