:: deftheorem defines -derivable FOMODEL4:def 12 :
for S being Language
for D being RuleSet of S
for Seqts being set holds
( Seqts is D -derivable iff Seqts is {} ,D -derivable );