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 object 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 object 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 :: thesis: for s being Element of Sts Q holds (Meas ((('not' p1) `1),s)) . (('not' p1) `2) = (Meas ((('not' q1) `1),s)) . (('not' q1) `2)

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;
1 - ((Meas ((p1 `1),s)) . E) = (Meas ((p1 `1),s)) . (p1 `2) by Th1
.= (Meas ((q1 `1),s)) . (q1 `2) by A7, Th2
.= 1 - ((Meas ((q1 `1),s)) . E1) by Th1 ;
hence (Meas ((('not' p1) `1),s)) . (('not' p1) `2) = (Meas ((('not' q1) `1),s)) . (('not' q1) `2) ; :: thesis: verum

end;

then A10: 'not' p1 <==> 'not' q1 by Th2;
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, Th7;
then [('not' q1),q] in PropRel Q by Def12;
hence 'not' q1 in C by A4, EQREL_1:19; :: thesis: verum