let MS be MusicSpace; :: thesis: for frequency being Element of MS holds Fifth (MS,frequency) is_Between frequency, Octave (MS,frequency)
let frequency be Element of MS; :: thesis: Fifth (MS,frequency) is_Between frequency, Octave (MS,frequency)
consider fr being positive Real such that
A1: ( frequency = fr & Fifth (MS,frequency) = (3 / 2) * fr ) by Def12;
A2: ex fr being positive Real st
( frequency = fr & Octave (MS,frequency) = 2 * fr ) by Def15;
reconsider x = (3 / 2) * fr as positive Real ;
( 1 * fr <= x & x < 2 * fr ) by XREAL_1:68;
hence Fifth (MS,frequency) is_Between frequency, Octave (MS,frequency) by A2, A1; :: thesis: verum