let Q be Quantum_Mechanics; :: thesis: OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantum_Logic
A1: OrdRel Q is_transitive_in Class (PropRel Q)

proof

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in Class (PropRel Q) or not y in Class (PropRel Q) or not z in Class (PropRel Q) or not [x,y] in OrdRel Q or not [y,z] in OrdRel Q or [x,z] in OrdRel Q )
assume that
A2: x in Class (PropRel Q) and
A3: y in Class (PropRel Q) and
A4: z in Class (PropRel Q) and
A5: ( [x,y] in OrdRel Q & [y,z] in OrdRel Q ) ; :: thesis: [x,z] in OrdRel Q
consider p being Element of Prop Q such that
A6: x = Class ((PropRel Q),p) by A2, EQREL_1:36;
consider r being Element of Prop Q such that
A7: z = Class ((PropRel Q),r) by A4, EQREL_1:36;
consider q being Element of Prop Q such that
A8: y = Class ((PropRel Q),q) by A3, EQREL_1:36;
( p |- q & q |- r implies p |- r ) by Th4;
hence [x,z] in OrdRel Q by A5, A6, A8, A7, Th10; :: thesis: verum

end;

A9: OrdRel Q is_antisymmetric_in Class (PropRel Q)

proof

let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in Class (PropRel Q) or not y in Class (PropRel Q) or not [x,y] in OrdRel Q or not [y,x] in OrdRel Q or x = y )
assume that
A10: x in Class (PropRel Q) and
A11: y in Class (PropRel Q) and
A12: ( [x,y] in OrdRel Q & [y,x] in OrdRel Q ) ; :: thesis: x = y
consider p being Element of Prop Q such that
A13: x = Class ((PropRel Q),p) by A10, EQREL_1:36;
consider q being Element of Prop Q such that
A14: y = Class ((PropRel Q),q) by A11, EQREL_1:36;
A15: ( p <==> q implies [p,q] in PropRel Q ) by Def12;
thus x = y by A12, A13, A14, A15, Th10, EQREL_1:35; :: thesis: verum

end;

A16: for x, y being Element of Class (PropRel Q) st [x,y] in OrdRel Q holds
[((InvRel Q) . y),((InvRel Q) . x)] in OrdRel Q

proof

let x, y be Element of Class (PropRel Q); :: thesis: ( [x,y] in OrdRel Q implies [((InvRel Q) . y),((InvRel Q) . x)] in OrdRel Q )
consider p being Element of Prop Q such that
A17: x = Class ((PropRel Q),p) by EQREL_1:36;
consider q being Element of Prop Q such that
A18: y = Class ((PropRel Q),q) by EQREL_1:36;
A19: ( p |- q implies 'not' q |- 'not' p ) by Th8;
( (InvRel Q) . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) & (InvRel Q) . (Class ((PropRel Q),q)) = Class ((PropRel Q),('not' q)) ) by Def14;
hence ( [x,y] in OrdRel Q implies [((InvRel Q) . y),((InvRel Q) . x)] in OrdRel Q ) by A17, A18, A19, Th10; :: thesis: verum

end;

A20: InvRel Q is_an_involution

proof

let x be Element of Class (PropRel Q); :: according to QMAX_1:def 6 :: thesis: (InvRel Q) . ((InvRel Q) . x) = x
consider p being Element of Prop Q such that
A21: x = Class ((PropRel Q),p) by EQREL_1:36;
(InvRel Q) . ((InvRel Q) . x) = (InvRel Q) . (Class ((PropRel Q),('not' p))) by A21, Def14
.= Class ((PropRel Q),('not' ('not' p))) by Def14 ;
hence (InvRel Q) . ((InvRel Q) . x) = x by A21; :: thesis: verum

end;

OrdRel Q is_reflexive_in Class (PropRel Q)

proof

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in Class (PropRel Q) or [x,x] in OrdRel Q )
assume x in Class (PropRel Q) ; :: thesis: [x,x] in OrdRel Q
then ex p being Element of Prop Q st x = Class ((PropRel Q),p) by EQREL_1:36;
hence [x,x] in OrdRel Q by Th10; :: thesis: verum

end;

then OrdRel Q partially_orders Class (PropRel Q) by A1, A9, ORDERS_1:def 8;
hence OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantum_Logic by A20, A16; :: thesis: verum