(pentatonic_pythagorean_scale (MS,frequency)) . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 by Def20;
hence (pentatonic_pythagorean_scale (MS,frequency)) . 2 is Element of MS ; :: thesis: verum