theorem Th137: :: FINSEQ_2:139

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