let x be Element of [:X1,X2,X3:]; :: thesis: x is triple
ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3] by Lm2;
hence x is triple ; :: thesis: verum