:: deftheorem defines -provable FOMODEL4:def 14 :
for S being Language
for D being RuleSet of S
for X, x being set holds
( x is X,D -provable iff ex seqt being object st
( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable ) );