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 B0: {(R . Seqts)} = Im (R,Seqts) by FUNCT_1:59
.= R .: {Seqts} ;
OneStep {R} c= (OneStep {R}) [*] by LANG1:18;
then B1: R c= (OneStep {R}) [*] by Lm8;
{(R . Seqts)} c= ((OneStep {R}) [*]) .: {Seqts} by B0, B1, RELAT_1:124;
then union {(R . Seqts)} c= union (((OneStep {R}) [*]) .: {Seqts}) by ZFMISC_1:77;
then B3: R . Seqts c= union (((OneStep {R}) [*]) .: {Seqts}) by ZFMISC_1:25;
assume Y c= R . Seqts ; :: thesis: Y is Seqts,{R} -derivable
then Y c= union (((OneStep {R}) [*]) .: {Seqts}) by B3, XBOOLE_1:1;
hence Y is Seqts,{R} -derivable by DefDerivable; :: thesis: verum