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 A1: ( 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 object such that
A2: ( seqt `1 c= X & seqt `2 = x & {seqt} is D1 -derivable ) ;
{seqt} is {} ,D2 -derivable by A2, A1, Lm18;
hence x is X,D2 -provable by A2; :: thesis: verum