let q1, q2 be Element of MS; :: thesis: ( [frequency,q1] in octave MS & [frequency,q2] in octave MS implies q1 = q2 )
assume that
A1: [frequency,q1] in octave MS and
A2: [frequency,q2] in octave MS ; :: thesis: q1 = q2
reconsider n1 = 1, n2 = 2 as Element of MS by Th20;
A3: n1,n2 equiv frequency,q1 by A1, EQREL_1:18;
n1,n2 equiv frequency,q2 by A2, EQREL_1:18;
then frequency,q2 equiv n1,n2 by Th22;
hence q1 = q2 by A3, Th23, Th24; :: thesis: verum