defpred S1[] means ex seqt being object st
( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable );
thus ( x is X,D -provable implies S1[] ) :: 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: S1[]
per cases ( {[X,x]} is D -derivable or not {[X,x]} is D -derivable ) ;
suppose A2: {[X,x]} is D -derivable ; :: thesis: S1[]
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;
end;
end;
assume S1[] ; :: thesis: x is X,D -provable
hence x is X,D -provable ; :: thesis: verum