let y be set ; :: thesis: ( y is x,D -provable implies y is X,D -provable )
assume y is x,D -provable ; :: thesis: y is X,D -provable
then consider seqt being set such that
B0: ( seqt `1 c= x & seqt `2 = y & {seqt} is D -derivable ) by DefProvable2;
( seqt `1 c= X & seqt `2 = y & {seqt} is D -derivable ) by B0, XBOOLE_1:1;
hence y is X,D -provable by DefProvable2; :: thesis: verum