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