for S being Language
for phi0 being 0wff string of S st (S -firstChar) . phi0 <> TheEqSymbOf S holds
phi0 is OwnSymbolsOf S -valued