set MS = REAL_Music ;
let frequency be Element of REAL_Music; :: according to MUSIC_S1:def 75 :: thesis: ex q being Element of REAL_Music st [frequency,q] in fourth REAL_Music
consider fr, qr being positive Real such that
A1: fr = frequency and
qr = (4 / 3) * fr and
A2: [fr,qr] in fourth REAL_Music by Th78;
( fr is Element of REAL_Music & qr is Element of REAL_Music ) by Th1;
hence ex q being Element of REAL_Music st [frequency,q] in fourth REAL_Music by A1, A2; :: thesis: verum