for m being Nat
for X, x being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) & x is m,X,D1 -derivable holds
x is m,X,D2 -derivable