theorem :: MUSIC_S1:95

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_reduct (MS,f1,f2) = f1