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