theorem Th99: :: FINSEQ_2:101

for D being non empty set
for d1, d2 being Element of D holds <*d1,d2*> in 2 -tuples_on D