for y being set
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