:: deftheorem Def11 defines -extension FOMODEL2:def 12 :
for S being Language
for U being non empty set
for I being b₁,b₂ -interpreter-like Function
for x being set holds
( x is I -extension iff x = I === );