for U being non empty set
for S1, S2 being Language st TheNorSymbOf S1 = TheNorSymbOf S2 & TheEqSymbOf S1 = TheEqSymbOf S2 & the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) holds
for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2
for phi1 being wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds
ex phi2 being wff string of S2 st
( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )