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 a, b, c, d being Element of Prop Q st a in B & b in B & c in C & d in C & a |- c holds
b |- d
let B, C be Subset of (Prop Q); :: thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) implies for a, b, c, d being Element of Prop Q st a in B & b in B & c in C & d in C & a |- c holds
b |- d )
assume that
A1: B in Class (PropRel Q) and
A2: C in Class (PropRel Q) ; :: thesis: for a, b, c, d being Element of Prop Q st a in B & b in B & c in C & d in C & a |- c holds
b |- d
let a, b, c, d be Element of Prop Q; :: thesis: ( a in B & b in B & c in C & d in C & a |- c implies b |- d )
assume that
A3: ( a in B & b in B ) and
A4: ( c in C & d in C ) ; :: thesis: ( not a |- c or b |- d )
assume A5: a |- c ; :: thesis: b |- d
let s be Element of Sts Q; :: according to QMAX_1:def 10 :: thesis: (Meas ((b `1),s)) . (b `2) <= (Meas ((d `1),s)) . (d `2)
ex y being object st
( y in Prop Q & C = Class ((PropRel Q),y) ) by A2, EQREL_1:def 3;
then [c,d] in PropRel Q by A4, EQREL_1:22;
then c <==> d by Def12;
then A6: (Meas ((c `1),s)) . (c `2) = (Meas ((d `1),s)) . (d `2) by Th2;
ex x being object st
( x in Prop Q & B = Class ((PropRel Q),x) ) by A1, EQREL_1:def 3;
then [a,b] in PropRel Q by A3, EQREL_1:22;
then a <==> b by Def12;
then (Meas ((a `1),s)) . (a `2) = (Meas ((b `1),s)) . (b `2) by Th2;
hence (Meas ((b `1),s)) . (b `2) <= (Meas ((d `1),s)) . (d `2) by A5, A6; :: thesis: verum