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