let m be Nat; :: thesis: for S being Language
for D1, D2 being RuleSet of S
for SQ1, SQ2 being b₁ -sequents-like set st SQ1 c= SQ2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . SQ1 c= ((m,D2) -derivables) . SQ2
let S be Language; :: thesis: for D1, D2 being RuleSet of S
for SQ1, SQ2 being S -sequents-like set st SQ1 c= SQ2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . SQ1 c= ((m,D2) -derivables) . SQ2
let D1, D2 be RuleSet of S; :: thesis: for SQ1, SQ2 being S -sequents-like set st SQ1 c= SQ2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . SQ1 c= ((m,D2) -derivables) . SQ2
let SQ1, SQ2 be S -sequents-like set ; :: thesis: ( SQ1 c= SQ2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) implies ((m,D1) -derivables) . SQ1 c= ((m,D2) -derivables) . SQ2 )
reconsider Seqts1 = SQ1, Seqts2 = SQ2 as Subset of (S -sequents) by Def3;
assume ( SQ1 c= SQ2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) ) ; :: thesis: ((m,D1) -derivables) . SQ1 c= ((m,D2) -derivables) . SQ2
then ((m,D1) -derivables) . Seqts1 c= ((m,D2) -derivables) . Seqts2 by Lm14;
hence ((m,D1) -derivables) . SQ1 c= ((m,D2) -derivables) . SQ2 ; :: thesis: verum