let MS be satisfying_equiv MusicStruct ; 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; ( 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 )
; 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; verum