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