theorem :: FOMODEL0:49

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;