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