:: deftheorem defines -AtomicEval FOMODEL2:def 13 :
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 holds I -AtomicEval phi = ((I ===) . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi));