:: deftheorem Def08a defines satisfying_equiv MUSIC_S1:def 13 :
for S being MusicStruct holds
( S is satisfying_equiv iff for f1, f2, f3, f4 being Element of S holds
( f1,f2 equiv f3,f4 iff the Ratio of S . (f1,f2) = the Ratio of S . (f3,f4) ) );