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