let m be Nat; :: thesis: for X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . X c= ((m,D2) -derivables) . X
let X be set ; :: thesis: for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . X c= ((m,D2) -derivables) . X
let S be Language; :: thesis: for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . X c= ((m,D2) -derivables) . X
let D1, D2 be RuleSet of S; :: thesis: ( D1 c= D2 & ( D2 is isotone or D1 is isotone ) implies ((m,D1) -derivables) . X c= ((m,D2) -derivables) . X )
set Q = S -sequents ;
set f1 = (m,D1) -derivables ;
set f2 = (m,D2) -derivables ;
assume A1: ( D1 c= D2 & ( D2 is isotone or D1 is isotone ) ) ; :: thesis: ((m,D1) -derivables) . X c= ((m,D2) -derivables) . X
per cases ( X in bool (S -sequents) or not X in bool (S -sequents) ) ;
suppose X in bool (S -sequents) ; :: thesis: ((m,D1) -derivables) . X c= ((m,D2) -derivables) . X
then reconsider Seqts1 = X as Element of bool (S -sequents) ;
((m,D1) -derivables) . Seqts1 c= ((m,D2) -derivables) . Seqts1 by Lm14, A1;
hence ((m,D1) -derivables) . X c= ((m,D2) -derivables) . X ; :: thesis: verum
end;
suppose not X in bool (S -sequents) ; :: thesis: ((m,D1) -derivables) . X c= ((m,D2) -derivables) . X
then ( not X in dom ((m,D1) -derivables) & not X in dom ((m,D2) -derivables) ) ;
then ( ((m,D1) -derivables) . X = {} & ((m,D2) -derivables) . X = {} ) by FUNCT_1:def 2;
hence ((m,D1) -derivables) . X c= ((m,D2) -derivables) . X ; :: thesis: verum
end;
end;