theorem Th48: :: PROOFS_1:10

for B, B1 being set
for R being Rule
for S being Formula-finset st S is B,R -derivable & B /\ S c= B1 holds
S is B1,R -derivable