take x1 ; :: thesis: for y1, y2 being set st x = [y1,y2] holds
x1 = y1
thus for y1, y2 being set st x = [y1,y2] holds
x1 = y1 by A1, ZFMISC_1:33; :: thesis: verum