:: deftheorem defines -witnessed FOMODEL4:def 65 :
for S being Language
for X being set holds
( X is S -witnessed iff for l1 being literal Element of S
for phi1 being wff string of S st <*l1*> ^ phi1 in X holds
ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in X & not l2 in rng phi1 ) );