theorem Th71: :: MUSIC_S1:94

for MS being MusicSpace
for fondamentale, f1, f2 being Element of MS
for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
( ( Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1 ) & ( not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,f2) = f1 ) )