let Q be Quantum_Mechanics; :: thesis: for p, q, r being Element of Prop Q st p |- q & q |- r holds
p |- r
let p, q, r be Element of Prop Q; :: thesis: ( p |- q & q |- r implies p |- r )
assume A1: ( p |- q & q |- r ) ; :: thesis: p |- r
let s be Element of Sts Q; :: according to QMAX_1:def 10 :: thesis: (Meas (p `1 ),s) . (p `2 ) <= (Meas (r `1 ),s) . (r `2 )
( (Meas (p `1 ),s) . (p `2 ) <= (Meas (q `1 ),s) . (q `2 ) & (Meas (q `1 ),s) . (q `2 ) <= (Meas (r `1 ),s) . (r `2 ) ) by A1, Def10;
hence (Meas (p `1 ),s) . (p `2 ) <= (Meas (r `1 ),s) . (r `2 ) by XXREAL_0:2; :: thesis: verum