let Q be Quantum_Mechanics; :: thesis: for p, q being Element of Prop Q st p |- q holds
'not' q |- 'not' p
let p, q be Element of Prop Q; :: thesis: ( p |- q implies 'not' q |- 'not' p )
assume A1: p |- q ; :: thesis: 'not' q |- 'not' p
let s be Element of Sts Q; :: according to QMAX_1:def 10 :: thesis: (Meas ((('not' q) `1),s)) . (('not' q) `2) <= (Meas ((('not' p) `1),s)) . (('not' p) `2)
reconsider E1 = (q `2) ` as Event of Borel_Sets by PROB_1:20;
reconsider E = (p `2) ` as Event of Borel_Sets by PROB_1:20;
set p1 = (Meas ((p `1),s)) . E;
set p2 = (Meas ((q `1),s)) . E1;
A2: ( - (1 - ((Meas ((p `1),s)) . E)) = ((Meas ((p `1),s)) . E) - 1 & - (1 - ((Meas ((q `1),s)) . E1)) = ((Meas ((q `1),s)) . E1) - 1 ) ;
A4: ( (Meas ((q `1),s)) . (q `2) = 1 - ((Meas ((q `1),s)) . E1) & (Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E) ) by Th1;
(Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2) by A1;
then ((Meas ((q `1),s)) . E1) - 1 <= ((Meas ((p `1),s)) . E) - 1 by A4, A2, XREAL_1:24;
hence (Meas ((('not' q) `1),s)) . (('not' q) `2) <= (Meas ((('not' p) `1),s)) . (('not' p) `2) by XREAL_1:9; :: thesis: verum