let Y be set ; 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; 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; 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); ( 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
; Y is Seqts,{R} -derivable
hence
Y is Seqts,{R} -derivable
by A3, XBOOLE_1:1; verum