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)

[((InvRel Q) . y),((InvRel Q) . x)] in OrdRel Q

hence OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantum_Logic by A20, A16; :: thesis: verum

A1: OrdRel Q is_transitive_in Class (PropRel Q)

proof

A9:
OrdRel Q is_antisymmetric_in Class (PropRel Q)
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;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

proof

A16:
for x, y being Element of Class (PropRel Q) st [x,y] in OrdRel Q holds
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;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

[((InvRel Q) . y),((InvRel Q) . x)] in OrdRel Q

proof

A20:
InvRel Q is_an_involution
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;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

proof

OrdRel Q is_reflexive_in Class (PropRel Q)
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;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

proof

then
OrdRel Q partially_orders Class (PropRel Q)
by A1, A9, ORDERS_1:def 8;
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;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

hence OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantum_Logic by A20, A16; :: thesis: verum