theorem :: FOMODEL2:19

for S being Language
for U being non empty set
for l being literal Element of S
for phi, phi1, phi2 being wff string of S
for I being Element of U -InterpretersOf S holds
( ( I -TruthEval (<*l*> ^ phi) = TRUE implies ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 ) & ( ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 implies I -TruthEval (<*l*> ^ phi) = TRUE ) & ( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE implies ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) ) & ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE implies I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE ) ) by Lm35, Lm37;