:: deftheorem Def27 defines perfect_fifth MUSIC_S1:def 89 :
for MS being MusicSpace
for n being natural Number
for scale being Element of n -tuples_on the carrier of MS st scale is heptatonic holds
( scale is perfect_fifth iff ( [(scale . 1),(scale . 5)] in fifth MS & [(scale . 2),(scale . 6)] in fifth MS & [(scale . 3),(scale . 7)] in fifth MS & [(scale . 4),(scale . 8)] in fifth MS ) );