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