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

proof

thus OrdRel Q is_reflexive_in Class (PropRel Q) :: according to ORDERS_1:def 7 :: thesis: ( OrdRel Q is_transitive_in Class (PropRel Q) & OrdRel Q is_antisymmetric_in Class (PropRel Q) )

proof

let x be set ; :: 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 consider p being Element of Prop Q such that
A2: x = Class (PropRel Q),p by EQREL_1:45;
p |- p by Th21;
hence [x,x] in OrdRel Q by A2, Th32; :: thesis: verum

end;

thus OrdRel Q is_transitive_in Class (PropRel Q) :: thesis: OrdRel Q is_antisymmetric_in Class (PropRel Q)

proof

let x be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in Class (PropRel Q) or not b₁ in Class (PropRel Q) or not b₂ in Class (PropRel Q) or not [x,b₁] in OrdRel Q or not [b₁,b₂] in OrdRel Q or [x,b₂] in OrdRel Q )
let y, z be set ; :: 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
A3: ( x in Class (PropRel Q) & y in Class (PropRel Q) & z in Class (PropRel Q) ) and
A4: ( [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
A5: x = Class (PropRel Q),p by A3, EQREL_1:45;
consider q being Element of Prop Q such that
A6: y = Class (PropRel Q),q by A3, EQREL_1:45;
consider r being Element of Prop Q such that
A7: z = Class (PropRel Q),r by A3, EQREL_1:45;
( p |- q & q |- r implies p |- r ) by Th22;
hence [x,z] in OrdRel Q by A4, A5, A6, A7, Th32; :: thesis: verum

end;

thus OrdRel Q is_antisymmetric_in Class (PropRel Q) :: thesis: verum

proof

let x be set ; :: according to RELAT_2:def 4 :: thesis: for b₁ being set holds
( not x in Class (PropRel Q) or not b₁ in Class (PropRel Q) or not [x,b₁] in OrdRel Q or not [b₁,x] in OrdRel Q or x = b₁ )
let y be set ; :: 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
A8: ( x in Class (PropRel Q) & y in Class (PropRel Q) ) and
A9: ( [x,y] in OrdRel Q & [y,x] in OrdRel Q ) ; :: thesis: x = y
consider p being Element of Prop Q such that
A10: x = Class (PropRel Q),p by A8, EQREL_1:45;
consider q being Element of Prop Q such that
A11: y = Class (PropRel Q),q by A8, EQREL_1:45;
( ( p |- q & q |- p implies p <==> q ) & ( p <==> q implies [p,q] in PropRel Q ) ) by Def11, Def12;
hence x = y by A9, A10, A11, Th32, EQREL_1:44; :: thesis: verum

end;

end;

A12: InvRel Q is_an_involution_in Class (PropRel Q)

proof

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

end;

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 r being Element of Prop Q;
consider p being Element of Prop Q such that
A14: x = Class (PropRel Q),p by EQREL_1:45;
consider q being Element of Prop Q such that
A15: y = Class (PropRel Q),q by EQREL_1:45;
A16: ( (InvRel Q) . (Class (PropRel Q),p) = Class (PropRel Q),('not' p) & (InvRel Q) . (Class (PropRel Q),q) = Class (PropRel Q),('not' q) ) by Def14;
( p |- q implies 'not' q |- 'not' p ) by Th28;
hence ( [x,y] in OrdRel Q implies [((InvRel Q) . y),((InvRel Q) . x)] in OrdRel Q ) by A14, A15, A16, Th32; :: thesis: verum

end;

hence OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantuum_Logic_on by A1, A12, Def7; :: thesis: verum