let frequency be Element of RAT_Music; :: thesis: ex r being positive Real st
( frequency = r & ( for n being non zero Nat holds n * r is Element of RAT_Music ) )
reconsider r = frequency as positive Rational by Th2;
take r ; :: thesis: ( frequency = r & ( for n being non zero Nat holds n * r is Element of RAT_Music ) )

now :: thesis: for n being non zero Nat holds n * r is Element of RAT_Music

let n be non zero Nat; :: thesis: n * r is Element of RAT_Music
n * r in RATPLUS ;
hence n * r is Element of RAT_Music ; :: thesis: verum

end;

hence ( frequency = r & ( for n being non zero Nat holds n * r is Element of RAT_Music ) ) ; :: thesis: verum