theorem :: FOMODEL3:5

for U1 being non empty set
for S being Language
for R being Equivalence_Relation of U1
for phi being 0wff string of S
for i being b₂,b₁ -interpreter-like b₃ -respecting Function st (S -firstChar) . phi <> TheEqSymbOf S holds
(i quotient R) -AtomicEval phi = i -AtomicEval phi by Lm26;