:: deftheorem defines WithWitnessesFrom FOMODEL4:def 72 :
for X being functional set
for S being Language
for D being RuleSet of S
for num being sequence of (ExFormulasOf S) holds X WithWitnessesFrom (D,num) = union (rng ((D,num) AddWitnessesTo X));