theorem :: FINSEQ_2:140

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