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
reconsider E = (p `2 ) ` as Event of Borel_Sets by PROB_1:50;
reconsider E1 = (q `2 ) ` as Event of Borel_Sets by PROB_1:50;
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 )
set p1 = (Meas (p `1 ),s) . E;
set p2 = (Meas (q `1 ),s) . E1;
A2: ( (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 Th16;
A3: ( - (1 - ((Meas (p `1 ),s) . E)) = ((Meas (p `1 ),s) . E) - 1 & - (1 - ((Meas (q `1 ),s) . E1)) = ((Meas (q `1 ),s) . E1) - 1 ) ;
(Meas (p `1 ),s) . (p `2 ) <= (Meas (q `1 ),s) . (q `2 ) by A1, Def10;
then A4: ((Meas (q `1 ),s) . E1) - 1 <= ((Meas (p `1 ),s) . E) - 1 by A2, A3, XREAL_1:26;
( ('not' q) `1 = q `1 & ('not' q) `2 = (q `2 ) ` & ('not' p) `1 = p `1 & ('not' p) `2 = (p `2 ) ` ) by MCART_1:7;
hence (Meas (('not' q) `1 ),s) . (('not' q) `2 ) <= (Meas (('not' p) `1 ),s) . (('not' p) `2 ) by A4, XREAL_1:11; :: thesis: verum