take {} (n -xtuples_of NAT) ; :: thesis: ( {} (n -xtuples_of NAT) is empty & {} (n -xtuples_of NAT) is diophantine )
thus ( {} (n -xtuples_of NAT) is empty & {} (n -xtuples_of NAT) is diophantine ) ; :: thesis: verum