for X, x being set
for S being Language
for D being RuleSet of S st x is X,D -provable holds
x is wff string of S by Lm25;