defpred S₁[] means ex seqt being object st
( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable );
thus ( x is X,D -provable implies S₁[] ) :: thesis: ( ex seqt being object st
( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable ) implies x is X,D -provable )

proof

assume A1: x is X,D -provable ; :: thesis: S₁[]

per cases ( {[X,x]} is D -derivable or not {[X,x]} is D -derivable ) ;

suppose A2: {[X,x]} is D -derivable ; :: thesis: S₁[]

reconsider seqt = [X,x] as set by TARSKI:1;
take seqt ; :: thesis: ( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable )
thus ( seqt `1 c= X & seqt `2 = x ) ; :: thesis: {seqt} is D -derivable
thus {seqt} is D -derivable by A2; :: thesis: verum

end;

suppose not {[X,x]} is D -derivable ; :: thesis: S₁[]

hence S₁[] by A1; :: thesis: verum

end;

end;

end;

assume S₁[] ; :: thesis: x is X,D -provable
hence x is X,D -provable ; :: thesis: verum