let Q be Quantum_Mechanics; 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); ( 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)
; 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; ( 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
; '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 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;
(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)
;
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; verum