:: deftheorem Def15 defines quotient FOMODEL3:def 15 :
for S being Language
for U being non empty set
for s being ofAtomicFormula Element of S
for E being Equivalence_Relation of U
for f being Interpreter of s,U holds
( ( not s is relational implies f quotient E = (|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),E)) ) & ( s is relational implies f quotient E = ((|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),(id BOOLEAN)))) * (peeler BOOLEAN) ) );