let D be non empty set ; :: thesis: for z being Element of 3 -tuples_on D ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>
let z be Element of 3 -tuples_on D; :: thesis: ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>
z in 3 -tuples_on D ;
then z in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } by Th122;
hence ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*> ; :: thesis: verum