let MS be satisfying_equiv MusicStruct ; :: thesis: for a, b being Element of MS holds a,b equiv a,b
let a, b be Element of MS; :: thesis: a,b equiv a,b
the Ratio of MS . (a,b) = the Ratio of MS . (a,b) ;
hence a,b equiv a,b by Def08a; :: thesis: verum