let x, X be set ; :: thesis: for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D1 is isotone or D2 is isotone ) & x is X,D1 -provable holds
x is X,D2 -provable
let S be Language; :: thesis: for D1, D2 being RuleSet of S st D1 c= D2 & ( D1 is isotone or D2 is isotone ) & x is X,D1 -provable holds
x is X,D2 -provable
let D1, D2 be RuleSet of S; :: thesis: ( D1 c= D2 & ( D1 is isotone or D2 is isotone ) & x is X,D1 -provable implies x is X,D2 -provable )
assume B1: ( D1 c= D2 & ( D1 is isotone or D2 is isotone ) ) ; :: thesis: ( not x is X,D1 -provable or x is X,D2 -provable )
assume x is X,D1 -provable ; :: thesis: x is X,D2 -provable
then consider seqt being set such that
B0: ( seqt `1 c= X & seqt `2 = x & {seqt} is D1 -derivable ) by DefProvable2;
{seqt} is {} ,D2 -derivable by B0, B1, Lm20;
hence x is X,D2 -provable by B0, DefProvable2; :: thesis: verum