theorem Th45: :: PROOFS_1:7

for B being set
for R being Rule
for t being object holds
( B,R |- t iff ex S being Formula-finset st
( t in S & S is B,R -derivable ) )