let Q be Quantum_Mechanics; :: thesis: for p, q being Element of Prop Q holds

( p <==> q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) )

let p, q be Element of Prop Q; :: thesis: ( p <==> q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) )

thus ( p <==> q implies for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) ) :: thesis: ( ( for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) ) implies p <==> q )

thus p |- q by A3; :: according to QMAX_1:def 11 :: thesis: q |- p

let s be Element of Sts Q; :: according to QMAX_1:def 10 :: thesis: (Meas ((q `1),s)) . (q `2) <= (Meas ((p `1),s)) . (p `2)

thus (Meas ((q `1),s)) . (q `2) <= (Meas ((p `1),s)) . (p `2) by A3; :: thesis: verum

( p <==> q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) )

let p, q be Element of Prop Q; :: thesis: ( p <==> q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) )

thus ( p <==> q implies for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) ) :: thesis: ( ( for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) ) implies p <==> q )

proof

assume A3:
for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2)
; :: thesis: p <==> q
assume A1:
p <==> q
; :: thesis: for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2)

let s be Element of Sts Q; :: thesis: (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2)

q |- p by A1;

then A2: (Meas ((q `1),s)) . (q `2) <= (Meas ((p `1),s)) . (p `2) ;

p |- q by A1;

then (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2) ;

hence (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) by A2, XXREAL_0:1; :: thesis: verum

end;let s be Element of Sts Q; :: thesis: (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2)

q |- p by A1;

then A2: (Meas ((q `1),s)) . (q `2) <= (Meas ((p `1),s)) . (p `2) ;

p |- q by A1;

then (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2) ;

hence (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) by A2, XXREAL_0:1; :: thesis: verum

thus p |- q by A3; :: according to QMAX_1:def 11 :: thesis: q |- p

let s be Element of Sts Q; :: according to QMAX_1:def 10 :: thesis: (Meas ((q `1),s)) . (q `2) <= (Meas ((p `1),s)) . (p `2)

thus (Meas ((q `1),s)) . (q `2) <= (Meas ((p `1),s)) . (p `2) by A3; :: thesis: verum