let Q be Quantum_Mechanics; :: thesis: for p being Element of Prop Q holds p |- p
let p be Element of Prop Q; :: thesis: p |- p
let s be Element of Sts Q; :: according to QMAX_1:def 10 :: thesis: (Meas (p `1 ),s) . (p `2 ) <= (Meas (p `1 ),s) . (p `2 )
thus (Meas (p `1 ),s) . (p `2 ) <= (Meas (p `1 ),s) . (p `2 ) ; :: thesis: verum