for X, x being set
for S being Language
for R being Rule of S st x in R . X holds
x is 1,X,{R} -derivable by Lm7;