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