theorem Th38: :: MUSIC_S1:46

for frequency being Element of REAL_Music ex fr being positive Real st
( frequency = fr & Fifth (REAL_Music,frequency) = (3 / 2) * fr )