theorem Th135: :: FINSEQ_2:137

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