(heptatonic_pythagorean_scale (HPS,frequency)) . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 by Def26;
hence (heptatonic_pythagorean_scale (HPS,frequency)) . 1 is Element of HPS ; :: thesis: verum