let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth MusicStruct ; :: thesis: for frequency being Element of MS ex r, s being positive Real st
( r = frequency & s = (3 / 2) * r & Fifth (MS,frequency) = s )
let frequency be Element of MS; :: thesis: ex r, s being positive Real st
( r = frequency & s = (3 / 2) * r & Fifth (MS,frequency) = s )
consider fr being positive Real such that
A1: ( frequency = fr & Fifth (MS,frequency) = (3 / 2) * fr ) by Def12;
reconsider s = (3 / 2) * fr as positive Real ;
take fr ; :: thesis: ex s being positive Real st
( fr = frequency & s = (3 / 2) * fr & Fifth (MS,frequency) = s )
take s ; :: thesis: ( fr = frequency & s = (3 / 2) * fr & Fifth (MS,frequency) = s )
thus ( fr = frequency & s = (3 / 2) * fr & Fifth (MS,frequency) = s ) by A1; :: thesis: verum