let S be Language; :: thesis: for Seqts being Subset of (S -sequents)
for seqt being Element of S -sequents
for R being Relation of (bool (S -sequents)),(S -sequents) st [Seqts,seqt] in R holds
seqt in (FuncRule R) . Seqts
let Seqts be Subset of (S -sequents); :: thesis: for seqt being Element of S -sequents
for R being Relation of (bool (S -sequents)),(S -sequents) st [Seqts,seqt] in R holds
seqt in (FuncRule R) . Seqts
let seqt be Element of S -sequents ; :: thesis: for R being Relation of (bool (S -sequents)),(S -sequents) st [Seqts,seqt] in R holds
seqt in (FuncRule R) . Seqts
let R be Relation of (bool (S -sequents)),(S -sequents); :: thesis: ( [Seqts,seqt] in R implies seqt in (FuncRule R) . Seqts )
A1: (FuncRule R) . Seqts = { x where x is Element of S -sequents : [Seqts,x] in R } by Def47;
assume [Seqts,seqt] in R ; :: thesis: seqt in (FuncRule R) . Seqts
hence seqt in (FuncRule R) . Seqts by A1; :: thesis: verum