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