:: deftheorem Def7 defines -derivable FOMODEL4:def 7 :
for S being Language
for D being RuleSet of S
for Seqs1 being object
for Seqs2 being set holds
( Seqs2 is Seqs1,D -derivable iff Seqs2 c= union (((OneStep D) [*]) .: {Seqs1}) );