let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct ; :: thesis: for fondamentale, frequency being Element of MS st frequency is_Between fondamentale, Octave (MS,fondamentale) holds
ex r1, r2, r3 being positive Real st
( fondamentale = r1 & frequency = r2 & Octave (MS,fondamentale) = 2 * r1 & r1 <= r2 & r2 <= 2 * r1 )
let fondamentale, frequency be Element of MS; :: thesis: ( frequency is_Between fondamentale, Octave (MS,fondamentale) implies ex r1, r2, r3 being positive Real st
( fondamentale = r1 & frequency = r2 & Octave (MS,fondamentale) = 2 * r1 & r1 <= r2 & r2 <= 2 * r1 ) )
assume A1: frequency is_Between fondamentale, Octave (MS,fondamentale) ; :: thesis: ex r1, r2, r3 being positive Real st
( fondamentale = r1 & frequency = r2 & Octave (MS,fondamentale) = 2 * r1 & r1 <= r2 & r2 <= 2 * r1 )
ex r9 being positive Real st
( fondamentale = r9 & Octave (MS,fondamentale) = 2 * r9 ) by Def15;
hence ex r1, r2, r3 being positive Real st
( fondamentale = r1 & frequency = r2 & Octave (MS,fondamentale) = 2 * r1 & r1 <= r2 & r2 <= 2 * r1 ) by A1; :: thesis: verum