for S being Language
for phi being wff string of S holds phi in AllFormulasOf S