for Q being Quantum_Mechanics
for s being Element of Sts Q
for p being Element of Prop Q
for E being Event of Borel_Sets st E = (p `2) ` holds
(Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E)