:: deftheorem defines -provable FOMODEL4:def 20 :
for S being Language
for D being RuleSet of S
for X, x being set holds
( x is X,D -provable iff ex H being set ex m being Nat st
( H c= X & [H,x] is m, {} ,D -derivable ) );