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

hereby :: thesis: ( c,d equiv a,b implies a,b equiv c,d )

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

end;

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