for MS being MusicSpace
for f1, f2 being Element of MS
for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
( Fifth (MS,f2) = 2 * r1 & not Fifth (MS,f2) is_Between f1, Octave (MS,f1) )