let frequency be Element of MS; :: thesis: ex f, qr being positive Real st
( f = frequency & qr = (4 / 3) * f & [f,qr] in fourth MS )
reconsider f = frequency as positive Real by A1, Th1;
reconsider qr = (4 / 3) * f as positive Real ;
reconsider q = qr as Element of MS by A1, Th1;
take f = f; :: thesis: ex qr being positive Real st
( f = frequency & qr = (4 / 3) * f & [f,qr] in fourth MS )
take qr = qr; :: thesis: ( f = frequency & qr = (4 / 3) * f & [f,qr] in fourth MS )
thus f = frequency ; :: thesis: ( qr = (4 / 3) * f & [f,qr] in fourth MS )
thus qr = (4 / 3) * f ; :: thesis: [f,qr] in fourth MS
reconsider n2 = 3, n3 = 4 as Element of MS by Th20;
reconsider x = [n2,n3], y = [frequency,q] as Element of [:REALPLUS,REALPLUS:] by A1;
reconsider z = [frequency,q] as Element of [:REALPLUS,REALPLUS:] by A1;
consider x9, y9 being Element of REALPLUS such that
A2: z = [x9,y9] and
A3: REAL_ratio . z = REAL_ratio (x9,y9) by Def02;
consider r, s being positive Real such that
A4: ( x9 = r & s = y9 & REAL_ratio (x9,y9) = s / r ) by Def01;
consider x99, y99 being Element of REALPLUS such that
A5: x = [x99,y99] and
A6: REAL_ratio . x = REAL_ratio (x99,y99) by Def02;
consider r9, s9 being positive Real such that
A7: ( x99 = r9 & s9 = y99 & REAL_ratio (x99,y99) = s9 / r9 ) by Def01;
A8: ( n2 = r9 & n3 = s9 & r = frequency & s = q ) by A4, A2, A5, A7, XTUPLE_0:1;
then n2,n3 equiv frequency,q by A1, Def08a;
hence [f,qr] in fourth MS by EQREL_1:18; :: thesis: verum