theorem :: FOMODEL3:6

for X being set
for S being Language
for a being ofAtomicFormula Element of S
for T being |.(ar b₃).| -element Element of (AllTermsOf S) * holds
( ( not a is relational implies (X -freeInterpreter a) . T = a -compound T ) & ( a is relational implies (X -freeInterpreter a) . T = (chi (X,(AtomicFormulasOf S))) . (a -compound T) ) )