theorem :: FINSEQ_2:138

for A being set
for a, b being object st <*a,b*> in 2 -tuples_on A holds
( a in A & b in A )