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 A1: ( B in Class (PropRel Q) & 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
let p1, q1 be Element of Prop Q; :: thesis: ( p1 in B & q1 in B & 'not' p1 in C implies 'not' q1 in C )
consider x being set such that
A2: ( x in Prop Q & B = Class (PropRel Q),x ) by A1, EQREL_1:def 5;
consider y being set such that
A3: ( y in Prop Q & C = Class (PropRel Q),y ) by A1, EQREL_1:def 5;
reconsider q = y as Element of Prop Q by A3;
assume ( p1 in B & q1 in B & 'not' p1 in C ) ; :: thesis: 'not' q1 in C
then ( [p1,q1] in PropRel Q & [('not' p1),q] in PropRel Q ) by A2, A3, EQREL_1:27, EQREL_1:30;
then A4: ( p1 <==> q1 & 'not' p1 <==> q ) by Def12;
then A5: ( p1 <==> q1 & q <==> 'not' p1 ) by Th24;

now

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

end;

then 'not' p1 <==> 'not' q1 by Th20;
then q <==> 'not' q1 by A5, Th25;
then [q,('not' q1)] in PropRel Q by Def12;
then [('not' q1),q] in PropRel Q by EQREL_1:12;
hence 'not' q1 in C by A3, EQREL_1:27; :: thesis: verum