:: deftheorem defines major_tone MUSIC_S1:def 40 :
for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds major_tone MS = Class ( the Equidistance of MS,[8,9]);