take [#] (n -xtuples_of NAT) ; :: thesis: ( not [#] (n -xtuples_of NAT) is empty & [#] (n -xtuples_of NAT) is diophantine )
thus ( not [#] (n -xtuples_of NAT) is empty & [#] (n -xtuples_of NAT) is diophantine ) ; :: thesis: verum