let frequency be Element of REAL_Music; :: according to MUSIC_S1:def 50 :: thesis: ex o being Element of REAL_Music st [o,frequency] in octave REAL_Music
consider fr, qr being positive Real such that
A2: fr = frequency and
qr = (1 / 2) * fr and
A4: [qr,fr] in octave REAL_Music by Th47;
( fr is Element of REAL_Music & qr is Element of REAL_Music ) by Th1;
hence ex o being Element of REAL_Music st [o,frequency] in octave REAL_Music by A2, A4; :: thesis: verum