let X, x be set ; :: thesis: 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; :: thesis: for R being Rule of S st x in R . X holds
x is 1,X,{R} -derivable
let R be Rule of S; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum