set MS = RAT_Music ;
let frequency be Element of RAT_Music; :: thesis: ex fr being positive Rational st
( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr )
reconsider fr = frequency as positive Rational by Th2;
take fr ; :: thesis: ( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr )
thus frequency = fr ; :: thesis: Fifth (RAT_Music,frequency) = (3 / 2) * fr
consider fr9, qr9 being positive Rational such that
A1: fr9 = frequency and
A2: qr9 = (3 / 2) * fr9 and
A3: [fr9,qr9] in fifth RAT_Music by Th36;
reconsider qr9 = qr9 as Element of RAT_Music by Th2;
qr9 = Fifth (RAT_Music,frequency) by A1, A3, Def11bis;
hence Fifth (RAT_Music,frequency) = (3 / 2) * fr by A1, A2; :: thesis: verum