set MS = RAT_Music ;
for frequency being Element of RAT_Music ex fr being positive Real st
( frequency = fr & Octave (RAT_Music,frequency) = 2 * fr )

proof

let frequency be Element of RAT_Music; :: thesis: ex fr being positive Real st
( frequency = fr & Octave (RAT_Music,frequency) = 2 * fr )
consider fr, qr being positive Rational such that
A1: fr = frequency and
A2: qr = 2 * fr and
A3: [fr,qr] in octave RAT_Music by Th43;
reconsider qr = qr as Element of RAT_Music by Th2;
[frequency,qr] in octave RAT_Music by A1, A3;
then Octave (RAT_Music,frequency) = 2 * fr by Def14, A2;
hence ex fr being positive Real st
( frequency = fr & Octave (RAT_Music,frequency) = 2 * fr ) by A1; :: thesis: verum

end;

hence RAT_Music is classical_octave ; :: thesis: verum