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