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

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

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

end;

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