let X, Y be 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
let S be 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
let D1, D2 be RuleSet of S; ( D1 c= D2 & ( D2 is isotone or D1 is isotone ) & Y is X,D1 -derivable implies Y is X,D2 -derivable )
set O1 = OneStep D1;
set O2 = OneStep D2;
set Q = S -sequents ;
set LH = union (((OneStep D1) [*]) .: {X});
set RH = union (((OneStep D2) [*]) .: {X});
assume
( D1 c= D2 & ( D2 is isotone or D1 is isotone ) & Y is X,D1 -derivable )
; Y is X,D2 -derivable
then
( union (((OneStep D1) [*]) .: {X}) c= union (((OneStep D2) [*]) .: {X}) & Y c= union (((OneStep D1) [*]) .: {X}) )
by Lm17;
hence
Y is X,D2 -derivable
by XBOOLE_1:1; verum