for m, n being Nat
for x, y, z being set
for S being Language
for D1, D2, D3 being RuleSet of S
for SQ1, SQ2 being b₆ -sequents-like set st D1 \/ D2 is isotone & (D1 \/ D2) \/ D3 is isotone & x is m,SQ1,D1 -derivable & y is m,SQ2,D2 -derivable & z is n,{x,y},D3 -derivable holds
z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable by Lm46;