:: deftheorem defines === FOMODEL2:def 11 :
for S being Language
for U being non empty set
for I being b₁,b₂ -interpreter-like Function holds I === = I +* ((TheEqSymbOf S) .--> (U -deltaInterpreter));