let S be Language; :: thesis: for SQ being S -sequents-like set
for Sq being S -sequent-like set
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 set
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 set ; :: 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 DefSeqtLike2;
reconsider seqt = Sq as Element of S -sequents by DefSeqtLike;
B0: FuncRule R = OneStep {(FuncRule R)} by Lm8
.= (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 B0, Lm1;
hence Sq is 1,SQ,{(FuncRule R)} -derivable by DefDerivable3; :: thesis: verum