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

proof

assume A3: Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) ; :: thesis: Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1
A4: ex fr being positive Real st
( f2 = fr & Fifth (MS,f2) = (3 / 2) * fr ) by Def12;
ex r being positive Real st
( Fifth_reduct (MS,fondamentale,f2) = r & Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = r / 2 ) by Th51;
then Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = (2 * r1) / 2 by A3, A4, Def18, A1, A2
.= f1 by A1 ;
hence Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1 ; :: thesis: verum

end;

thus ( not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,f2) = f1 ) :: thesis: verum

proof

assume A5: not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) ; :: thesis: Fifth_reduct (MS,fondamentale,f2) = f1
consider fr being positive Real such that
A6: ( f2 = fr & Fifth (MS,f2) = (3 / 2) * fr ) by Def12;
ex r being positive Real st
( Fifth (MS,f2) = r & Octave_descendent (MS,(Fifth (MS,f2))) = r / 2 ) by Th51;
hence Fifth_reduct (MS,fondamentale,f2) = f1 by A1, A2, A6, A5, Def18; :: thesis: verum

end;