let Q be Quantum_Mechanics; :: thesis: for B, C being Subset of (Prop Q) st B in Class (PropRel Q) & C in Class (PropRel Q) holds
for p1, q1 being Element of Prop Q st p1 in B & q1 in B & 'not' p1 in C holds
'not' q1 in C
let B, C be Subset of (Prop Q); :: thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) implies for p1, q1 being Element of Prop Q st p1 in B & q1 in B & 'not' p1 in C holds
'not' q1 in C )
assume that
A1: B in Class (PropRel Q) and
A2: C in Class (PropRel Q) ; :: thesis: for p1, q1 being Element of Prop Q st p1 in B & q1 in B & 'not' p1 in C holds
'not' q1 in C
consider y being set such that
A3: y in Prop Q and
A4: C = Class ((PropRel Q),y) by A2, EQREL_1:def 3;
let p1, q1 be Element of Prop Q; :: thesis: ( p1 in B & q1 in B & 'not' p1 in C implies 'not' q1 in C )
assume that
A5: ( p1 in B & q1 in B ) and
A6: 'not' p1 in C ; :: thesis: 'not' q1 in C
ex x being set st
( x in Prop Q & B = Class ((PropRel Q),x) ) by A1, EQREL_1:def 3;
then [p1,q1] in PropRel Q by A5, EQREL_1:22;
then A7: p1 <==> q1 by Def12;

now

reconsider E1 = (q1 `2) ` , E = (p1 `2) ` as Event of Borel_Sets by PROB_1:20;
let s be Element of Sts Q; :: thesis: (Meas ((('not' p1) `1),s)) . (('not' p1) `2) = (Meas ((('not' q1) `1),s)) . (('not' q1) `2)
set r1 = (Meas ((p1 `1),s)) . E;
set r2 = (Meas ((q1 `1),s)) . E1;
A8: ( ('not' p1) `1 = p1 `1 & ('not' p1) `2 = (p1 `2) ` ) by MCART_1:7;
A9: ('not' q1) `1 = q1 `1 by MCART_1:7;
1 - ((Meas ((p1 `1),s)) . E) = (Meas ((p1 `1),s)) . (p1 `2) by Th16
.= (Meas ((q1 `1),s)) . (q1 `2) by A7, Th20
.= 1 - ((Meas ((q1 `1),s)) . E1) by Th16 ;
hence (Meas ((('not' p1) `1),s)) . (('not' p1) `2) = (Meas ((('not' q1) `1),s)) . (('not' q1) `2) by A8, A9, MCART_1:7; :: thesis: verum

end;

then A10: 'not' p1 <==> 'not' q1 by Th20;
reconsider q = y as Element of Prop Q by A3;
[('not' p1),q] in PropRel Q by A4, A6, EQREL_1:19;
then 'not' p1 <==> q by Def12;
then q <==> 'not' q1 by A10, Th25;
then [('not' q1),q] in PropRel Q by Def12;
hence 'not' q1 in C by A4, EQREL_1:19; :: thesis: verum