let B, B1 be set ; :: thesis: 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
let R be Rule; :: thesis: for S being Formula-finset st S is B,R -derivable & B /\ S c= B1 holds
S is B1,R -derivable
let S be Formula-finset; :: thesis: ( S is B,R -derivable & B /\ S c= B1 implies S is B1,R -derivable )
assume that
A1: S is B,R -derivable and
A2: B /\ S c= B1 ; :: thesis: S is B1,R -derivable
consider P being Formula-sequence such that
A3: S = rng P and
A4: P is B,R -correct by A1;
P is B1,R -correct

proof

let k be Nat; :: according to PROOFS_1:def 7 :: thesis: ( k in dom P implies P,k is_a_correct_step_wrt B1,R )
assume A6: k in dom P ; :: thesis: P,k is_a_correct_step_wrt B1,R
then A7: P . k in S by A3, FUNCT_1:3;
P,k is_a_correct_step_wrt B,R by A4, A6;

per cases then ( P . k in B or ex Q being Formula-finset st
( [Q,(P . k)] in R & ( for t being object st t in Q holds
ex m being Nat st
( m in dom P & m < k & P . m = t ) ) ) ) ;

suppose P . k in B ; :: thesis: P,k is_a_correct_step_wrt B1,R

then P . k in B /\ S by A7, XBOOLE_0:def 4;
hence P,k is_a_correct_step_wrt B1,R by A2; :: thesis: verum

end;

suppose ex Q being Formula-finset st
( [Q,(P . k)] in R & ( for t being object st t in Q holds
ex m being Nat st
( m in dom P & m < k & P . m = t ) ) ) ; :: thesis: P,k is_a_correct_step_wrt B1,R

then consider Q being Formula-finset such that
A10: [Q,(P . k)] in R and
A11: for t being object st t in Q holds
ex m being Nat st
( m in dom P & m < k & P . m = t ) ;
thus P,k is_a_correct_step_wrt B1,R by A10, A11; :: thesis: verum

end;

end;

end;

hence S is B1,R -derivable by A3; :: thesis: verum