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