let Y be set ; :: thesis: for S being Language
for R being Rule of S
for Seqts being Subset of (S -sequents) st Y c= R . Seqts holds
Y is Seqts,{R} -derivable
let S be Language; :: thesis: for R being Rule of S
for Seqts being Subset of (S -sequents) st Y c= R . Seqts holds
Y is Seqts,{R} -derivable
let R be Rule of S; :: thesis: for Seqts being Subset of (S -sequents) st Y c= R . Seqts holds
Y is Seqts,{R} -derivable
let Seqts be Subset of (S -sequents); :: thesis: ( Y c= R . Seqts implies Y is Seqts,{R} -derivable )
set D = {R};
set RR = (OneStep {R}) [*] ;
set Q = S -sequents ;
( Seqts in bool (S -sequents) & dom R = bool (S -sequents) ) by FUNCT_2:def 1;
then A1: {(R . Seqts)} = Im (R,Seqts) by FUNCT_1:59
.= R .: {Seqts} ;
OneStep {R} c= (OneStep {R}) [*] by LANG1:18;
then A2: R c= (OneStep {R}) [*] by Lm6;
{(R . Seqts)} c= ((OneStep {R}) [*]) .: {Seqts} by A1, A2, RELAT_1:124;
then union {(R . Seqts)} c= union (((OneStep {R}) [*]) .: {Seqts}) by ZFMISC_1:77;
then A3: R . Seqts c= union (((OneStep {R}) [*]) .: {Seqts}) ;
assume Y c= R . Seqts ; :: thesis: Y is Seqts,{R} -derivable
hence Y is Seqts,{R} -derivable by A3, XBOOLE_1:1; :: thesis: verum