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