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