for X, x being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D1 is isotone or D2 is isotone ) & x is X,D1 -provable holds
x is X,D2 -provable by Lm19;