:: deftheorem Def18 defines -expanded FOMODEL4:def 18 :
for S being Language
for D being RuleSet of S
for X being set holds
( X is D -expanded iff for x being set st x is X,D -provable holds
x in X );