let MS be satisfying_equiv MusicStruct ; :: thesis: for a, b, c, d, e, f being Element of MS st a,b equiv c,d & c,d equiv e,f holds
a,b equiv e,f
let a, b, c, d, e, f be Element of MS; :: thesis: ( a,b equiv c,d & c,d equiv e,f implies a,b equiv e,f )
assume ( a,b equiv c,d & c,d equiv e,f ) ; :: thesis: a,b equiv e,f
then ( the Ratio of MS . (a,b) = the Ratio of MS . (c,d) & the Ratio of MS . (c,d) = the Ratio of MS . (e,f) ) by Def08a;
hence a,b equiv e,f by Def08a; :: thesis: verum