:: deftheorem defines -derivable PROOFS_1:def 8 :
for B being set
for R being Rule
for S being Formula-finset holds
( S is B,R -derivable iff ex P being Formula-sequence st
( S = rng P & P is B,R -correct ) );