for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth MusicStruct
for frequency being Element of MS ex r, s being positive Real st
( r = frequency & s = (3 / 2) * r & Fifth (MS,frequency) = s )