theorem :: FOMODEL4:20

for X being set
for C being countable Language
for phi being wff string of C st X c= AllFormulasOf C & phi is X -implied holds
phi is X -provable