theorem :: FOMODEL2:15

for S being Language
for U being non empty set
for I being b₁,b₂ -interpreter-like Function
for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds
( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )