let S be satisfying_equiv satisfying_tonic MusicStruct ; :: thesis: for a, b, c being Element of S st a,a equiv b,c holds
b = c
let a, b, c be Element of S; :: thesis: ( a,a equiv b,c implies b = c )
assume a,a equiv b,c ; :: thesis: b = c
then the Ratio of S . (a,a) = the Ratio of S . (b,c) by Def08a;
hence b = c by Def10a; :: thesis: verum