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 )

proof

assume p <==> q ; :: thesis: for s being Element of Sts Q holds (Meas (p `1 ),s) . (p `2 ) = (Meas (q `1 ),s) . (q `2 )
then A1: ( p |- q & q |- p ) by Def11;
let s be Element of Sts Q; :: thesis: (Meas (p `1 ),s) . (p `2 ) = (Meas (q `1 ),s) . (q `2 )
( (Meas (p `1 ),s) . (p `2 ) <= (Meas (q `1 ),s) . (q `2 ) & (Meas (q `1 ),s) . (q `2 ) <= (Meas (p `1 ),s) . (p `2 ) ) by A1, Def10;
hence (Meas (p `1 ),s) . (p `2 ) = (Meas (q `1 ),s) . (q `2 ) by XXREAL_0:1; :: thesis: verum

end;

assume A2: for s being Element of Sts Q holds (Meas (p `1 ),s) . (p `2 ) = (Meas (q `1 ),s) . (q `2 ) ; :: thesis: p <==> q
thus p |- q :: according to QMAX_1:def 11 :: thesis: q |- p

proof

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

end;

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 A2; :: thesis: verum