take x3 ; :: thesis: for y1, y2, y3 being set st x = [y1,y2,y3] holds
x3 = y3
thus for y1, y2, y3 being set st x = [y1,y2,y3] holds
x3 = y3 by A1, MCART_1:28; :: thesis: verum