theorem :: MUSIC_S1:51

for MS being non empty satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct
for frequency being Element of MS ex seq being sequence of MS st
( seq . 0 = frequency & ( for n being Nat holds [(seq . n),(seq . (n + 1))] in fifth MS ) )