:: deftheorem defines -derivable FOMODEL4:def 8 :
for m being Nat
for S being Language
for D being RuleSet of S
for Seqts being set
for seqt being object holds
( seqt is m,Seqts,D -derivable iff seqt in ((m,D) -derivables) . Seqts );