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