theorem :: FOMODEL4:8

for m, n being Nat
for X, y, z being set
for S being Language
for D1, D2 being RuleSet of S st D1 is isotone & D1 \/ D2 is isotone & y is m,X,D1 -derivable & z is n,{y},D2 -derivable holds
z is m + n,X,D1 \/ D2 -derivable by Lm22;