let X, x be set ; for S being Language
for R being Rule of S st x in R . X holds
x is 1,X,{R} -derivable
let S be Language; for R being Rule of S st x in R . X holds
x is 1,X,{R} -derivable
let R be Rule of S; ( x in R . X implies x is 1,X,{R} -derivable )
set Q = S -sequents ;
set D = {R};
set O = OneStep {R};
set f = iter ((OneStep {R}),1);
assume A1:
x in R . X
; x is 1,X,{R} -derivable
then
X in dom R
by FUNCT_1:def 2;
then reconsider Seqts = X as Element of bool (S -sequents) ;
iter ((OneStep {R}),1) =
OneStep {R}
by FUNCT_7:70
.=
R
by Lm6
;
then
x in ((1,{R}) -derivables) . Seqts
by A1;
hence
x is 1,X,{R} -derivable
; verum