:: deftheorem defines -derivable PROOFS_1:def 15 :
for B being set
for R, R1 being Rule holds
( R1 is B,R -derivable iff for S being Formula-finset
for t being object st [S,t] in R1 holds
B \/ S,R |- t );