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