let MS be MusicSpace; :: thesis: 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
let f1, f2 be Element of MS; :: thesis: for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
Fifth_reduct (MS,f1,f2) = f1
let r1, r2 be positive Real; :: thesis: ( f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 implies Fifth_reduct (MS,f1,f2) = f1 )
assume A1: ( f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 ) ; :: thesis: Fifth_reduct (MS,f1,f2) = f1
then ( ( Fifth (MS,f2) is_Between f1, Octave (MS,f1) implies Octave_descendent (MS,(Fifth_reduct (MS,f1,f2))) = f1 ) & ( not Fifth (MS,f2) is_Between f1, Octave (MS,f1) implies Fifth_reduct (MS,f1,f2) = f1 ) ) by Th71;
hence Fifth_reduct (MS,f1,f2) = f1 by A1, Th70; :: thesis: verum