for HPS being satisfying_euclidean Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds
( [((heptatonic_pythagorean_scale (HPS,frequency)) . 5),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2)] in fifth HPS & [((heptatonic_pythagorean_scale (HPS,frequency)) . 6),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3)] in fifth HPS & not [((heptatonic_pythagorean_scale (HPS,frequency)) . 7),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4)] in fifth HPS )