let Q be Quantum_Mechanics; :: thesis: for B, C being Subset of (Prop Q) st B in Class () & C in Class () 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 () & C in Class () 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 () and
A2: C in Class () ; :: 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 ((),y) ) by ;
then [c,d] in PropRel Q by ;
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 ((),x) ) by ;
then [a,b] in PropRel Q by ;
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