:: deftheorem Def18 defines Fifth_reduct MUSIC_S1:def 52 :
for MS being satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible satisfying_octave_descendent_constructible MusicStruct
for fondamentale, frequency being Element of MS holds
( ( Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,frequency) = Fifth (MS,frequency) ) & ( not Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,frequency) = Octave_descendent (MS,(Fifth (MS,frequency))) ) );