theorem Th47: :: PROOFS_1:9

for B being set
for R being Rule
for S being Formula-finset st ( for a being object st a in S holds
B,R |- a ) holds
ex S1 being Formula-finset st
( S c= S1 & S1 is B,R -derivable )