theorem :: FOMODEL4:4

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