theorem Th90: :: MUSIC_S1:111

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds
( intrval ((hepta_fondamental (HPS,frequency)),(hepta_1 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_1 (HPS,frequency)),(hepta_2 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_2 (HPS,frequency)),(hepta_3 (HPS,frequency))) = heptatonic_pythagorean_semitone & intrval ((hepta_3 (HPS,frequency)),(hepta_4 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_4 (HPS,frequency)),(hepta_5 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_5 (HPS,frequency)),(hepta_6 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_6 (HPS,frequency)),(hepta_octave (HPS,frequency))) = heptatonic_pythagorean_semitone )