:: deftheorem Def3 defines -freeInterpreter FOMODEL3:def 3 :
for S being Language
for s being ofAtomicFormula Element of S
for X being set holds
( ( not s is relational implies X -freeInterpreter s = (s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) ) & ( s is relational implies X -freeInterpreter s = ((s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S))) * (chi (X,(AtomicFormulasOf S))) ) );