now :: thesis:

thus RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible MusicStruct ; :: thesis:
for frequency being Element of RAT_Music ex fr being positive Real st
( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr )

proof

let frequency be Element of RAT_Music; :: thesis:
ex fr being positive Rational st
( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr ) by Th39;
hence ex fr being positive Real st
( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr ) ; :: thesis:

end;

hence RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible classical_fifth MusicStruct by Def12; :: thesis:

end;

hence RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible classical_fifth MusicStruct ; :: thesis: