:: deftheorem Def12 defines classical_fifth MUSIC_S1:def 44 :
for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct holds
( MS is classical_fifth iff for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Fifth (MS,frequency) = (3 / 2) * fr ) );