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 is 1,SQ,{(FuncRule R)} -derivable
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 is 1,SQ,{(FuncRule R)} -derivable
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 is 1,SQ,{(FuncRule R)} -derivable
set Q = S -sequents ;
let R be Relation of (bool (S -sequents)),(S -sequents); :: thesis: ( [SQ,Sq] in R implies Sq is 1,SQ,{(FuncRule R)} -derivable )
set F = FuncRule R;
set O = OneStep {(FuncRule R)};
reconsider Seqts = SQ as Subset of (S -sequents) by Def3;
reconsider seqt = Sq as Element of S -sequents by Def2;
A1: FuncRule R = OneStep {(FuncRule R)} by Lm6
.= (1,{(FuncRule R)}) -derivables by FUNCT_7:70 ;
assume [SQ,Sq] in R ; :: thesis: Sq is 1,SQ,{(FuncRule R)} -derivable
then seqt in ((1,{(FuncRule R)}) -derivables) . Seqts by A1, Lm27;
hence Sq is 1,SQ,{(FuncRule R)} -derivable ; :: thesis: verum