:: deftheorem defines fifth MUSIC_S1:def 34 :
for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds fifth MS = Class ( the Equidistance of MS,[2,3]);