for X, Y, x being set
for S being Language
for D being RuleSet of S st X c= Y & x is X,D -provable holds
x is Y,D -provable ;