theorem Th88BIS: :: MUSIC_S1:108

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds heptatonic_pythagorean_scale (HPS,frequency) is heptatonic