:: deftheorem defines -satisfying FOMODEL2:def 43 :
for S being Language
for U being non empty set
for X being set
for I being Element of U -InterpretersOf S holds
( I is X -satisfying iff X is I -satisfied );