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

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