let HPS be Heptatonic_Pythagorean_Score; :: thesis: for frequency being Element of HPS holds Fourth (HPS,frequency) is_Between frequency, Octave (HPS,frequency)
let frequency be Element of HPS; :: thesis: Fourth (HPS,frequency) is_Between frequency, Octave (HPS,frequency)
set MS = HPS;
consider fr being positive Real such that
A1: frequency = fr and
A2: Fourth (HPS,frequency) = (4 / 3) * fr by Def24;
consider fr2 being positive Real such that
A3: frequency = fr2 and
A4: Octave (HPS,frequency) = 2 * fr2 by Def15;
( 1 * fr <= (4 / 3) * fr & (4 / 3) * fr < 2 * fr ) by XREAL_1:68;
hence Fourth (HPS,frequency) is_Between frequency, Octave (HPS,frequency) by A3, A4, A1, A2; :: thesis: verum