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 A1: 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
A2: ( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable ) by Def13;
( seqt `1 c= Y & seqt `2 = x & {seqt} is D -derivable ) by A2, A1, XBOOLE_1:1;
hence x is Y,D -provable by Def13; :: thesis: verum