:: deftheorem Def11a defines satisfying_commutativity MUSIC_S1:def 16 :
for S being MusicStruct holds
( S is satisfying_commutativity iff for f1, f2, f3, f4 being Element of S holds
( the Ratio of S . (f1,f2) = the Ratio of S . (f3,f4) iff the Ratio of S . (f2,f1) = the Ratio of S . (f4,f3) ) );