theorem Th133: :: FINSEQ_2:135

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