let q1, q2 be Element of MS; ( [frequency,q1] in fourth MS & [frequency,q2] in fourth MS implies q1 = q2 )
assume that
A1:
[frequency,q1] in fourth MS
and
A2:
[frequency,q2] in fourth MS
; q1 = q2
reconsider n2 = 3, n3 = 4 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 Th24, A3, Th23; verum