:: deftheorem defines CompletionOf FOMODEL4:def 75 :
for X being set
for S being Language
for D being RuleSet of S
for num being sequence of (AllFormulasOf S) holds (D,num) CompletionOf X = union (rng ((D,num) AddFormulasTo X));