let S be satisfying_equiv satisfying_interval MusicStruct ; :: thesis: for a, b, c being Element of S holds
( a,b equiv a,c iff b = c )
let a, b, c be Element of S; :: thesis: ( a,b equiv a,c iff b = c )

now :: thesis: ( a,b equiv a,c implies b = c )

assume a,b equiv a,c ; :: thesis: b = c
then the Ratio of S . (a,b) = the Ratio of S . (a,c) by Def08a;
hence b = c by Def09a; :: thesis: verum

end;

hence ( a,b equiv a,c iff b = c ) by Th21; :: thesis: verum