let y be set ; :: thesis: for S being Language
for D being RuleSet of S
for SQ being b₁ -sequents-like set st {y} is SQ,D -derivable holds
ex mm being Element of NAT st y is mm,SQ,D -derivable
let S be Language; :: thesis: for D being RuleSet of S
for SQ being S -sequents-like set st {y} is SQ,D -derivable holds
ex mm being Element of NAT st y is mm,SQ,D -derivable
let D be RuleSet of S; :: thesis: for SQ being S -sequents-like set st {y} is SQ,D -derivable holds
ex mm being Element of NAT st y is mm,SQ,D -derivable
let SQ be S -sequents-like set ; :: thesis: ( {y} is SQ,D -derivable implies ex mm being Element of NAT st y is mm,SQ,D -derivable )
set Q = S -sequents ;
reconsider Seqts = SQ as Element of bool (S -sequents) by Def3;
( {y} is Seqts,D -derivable implies ex mm being Element of NAT st y is mm,Seqts,D -derivable ) by Lm8;
hence ( {y} is SQ,D -derivable implies ex mm being Element of NAT st y is mm,SQ,D -derivable ) ; :: thesis: verum