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;

hence (Meas ((p `1),s)) . (p `2) <= (Meas ((r `1),s)) . (r `2) by XXREAL_0:2; :: thesis: verum

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;

hence (Meas ((p `1),s)) . (p `2) <= (Meas ((r `1),s)) . (r `2) by XXREAL_0:2; :: thesis: verum