let q1, q2 be Element of MS; ( [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
; 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; verum