for frequency being Element of RAT_Music ex r being positive Real st
( frequency = r & ( for n being non zero Nat holds n * r is Element of RAT_Music ) )