for U being non empty set
for S2 being Language
for X2 being countable Subset of (AllFormulasOf S2)
for I2 being Element of U -InterpretersOf S2 st X2 is I2 -satisfied holds
ex U1 being non empty countable set ex I1 being Element of U1 -InterpretersOf S2 st X2 is I1 -satisfied