let MS be non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct ; :: thesis: for frequency being Element of MS ex r being positive Real st
( frequency = r & Octave_descendent (MS,frequency) = r / 2 )
let frequency be Element of MS; :: thesis: ex r being positive Real st
( frequency = r & Octave_descendent (MS,frequency) = r / 2 )
A1: the carrier of MS c= REALPLUS by Def07a;
then reconsider r = frequency as positive Real by Th1;
reconsider r2 = r / 2 as positive Real ;
set ff = Octave_descendent (MS,frequency);
reconsider rff = Octave_descendent (MS,frequency) as positive Real by A1, Th1;
A2: ( [(Octave_descendent (MS,frequency)),frequency] in octave MS & [(Octave_descendent (MS,frequency)),(Octave (MS,(Octave_descendent (MS,frequency))))] in octave MS ) by Def14, Def17;
ex fr being positive Real st
( Octave_descendent (MS,frequency) = fr & Octave (MS,(Octave_descendent (MS,frequency))) = 2 * fr ) by Def15;
then frequency = 2 * rff by A2, Def14;
then rff = r / 2 ;
hence ex r being positive Real st
( frequency = r & Octave_descendent (MS,frequency) = r / 2 ) ; :: thesis: verum