theorem Th16: :: FOMODEL2:16

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