let X, Y 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 ) & Y is X,D1 -derivable holds
Y is X,D2 -derivable
let S be Language; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum