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

proof

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

end;

hence REAL_Music is classical_octave ; :: thesis: verum