let m be Nat; :: thesis: for X, 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 ) & x is m,X,D1 -derivable holds
x is m,X,D2 -derivable
let X, 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 ) & x is m,X,D1 -derivable holds
x is m,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 ) & x is m,X,D1 -derivable holds
x is m,X,D2 -derivable
let D1, D2 be RuleSet of S; :: thesis: ( D1 c= D2 & ( D2 is isotone or D1 is isotone ) & x is m,X,D1 -derivable implies x is m,X,D2 -derivable )
set f1 = (m,D1) -derivables ;
set f2 = (m,D2) -derivables ;
assume ( D1 c= D2 & ( D2 is isotone or D1 is isotone ) ) ; :: thesis: ( not x is m,X,D1 -derivable or x is m,X,D2 -derivable )
then A1: ((m,D1) -derivables) . X c= ((m,D2) -derivables) . X by Lm16;
assume x is m,X,D1 -derivable ; :: thesis: x is m,X,D2 -derivable
then x in ((m,D1) -derivables) . X ;
hence x is m,X,D2 -derivable by A1; :: thesis: verum