let S be Language; :: thesis: for SQ being S -sequents-like set
for Sq being S -sequent-like object
for R being Relation of (bool (S -sequents)),(S -sequents) st [SQ,Sq] in R holds
Sq in (FuncRule R) . SQ
let SQ be S -sequents-like set ; :: thesis: for Sq being S -sequent-like object
for R being Relation of (bool (S -sequents)),(S -sequents) st [SQ,Sq] in R holds
Sq in (FuncRule R) . SQ
let Sq be S -sequent-like object ; :: thesis: for R being Relation of (bool (S -sequents)),(S -sequents) st [SQ,Sq] in R holds
Sq in (FuncRule R) . SQ
set Q = S -sequents ;
reconsider seqt = Sq as Element of S -sequents by Def2;
reconsider Seqts = SQ as Element of bool (S -sequents) by Def3;
let R be Relation of (bool (S -sequents)),(S -sequents); :: thesis: ( [SQ,Sq] in R implies Sq in (FuncRule R) . SQ )
( [Seqts,seqt] in R implies seqt in (FuncRule R) . Seqts ) by Lm27;
hence ( [SQ,Sq] in R implies Sq in (FuncRule R) . SQ ) ; :: thesis: verum