let S be Subset of (n -xtuples_of NAT); :: thesis: S is diophantine

per cases ( S = {} or S <> 0 ) ;

suppose S = {} ; :: thesis: S is diophantine

hence S is diophantine ; :: thesis: verum

end;

suppose S <> 0 ; :: thesis: S is diophantine

then consider x being object such that
A1: x in S by XBOOLE_0:def 1;
reconsider x = x as n -element XFinSequence of NAT by A1;
n -xtuples_of NAT c= S by A1;
then [#] (n -xtuples_of NAT) = S by XBOOLE_0:def 10;
hence S is diophantine ; :: thesis: verum

end;

end;