let D be non empty set ; :: thesis: for d1, d2 being Element of D holds <*d1,d2*> in 2 -tuples_on D
let d1, d2 be Element of D; :: thesis: <*d1,d2*> in 2 -tuples_on D
<*d1,d2*> in { <*c1,c2*> where c1, c2 is Element of D : verum } ;
hence <*d1,d2*> in 2 -tuples_on D by Th97; :: thesis: verum