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