for m being Nat
for X, x being set
for S being Language
for D being RuleSet of S st x is m,X,D -derivable holds
{x} is X,D -derivable by Lm12;