for A, B being set
for m, n being Nat st m -tuples_on A meets n -tuples_on B holds
m = n by Lm5;