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