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