let x1, x2, y1, y2 be set ; :: thesis: ( [x1,x2] = [y1,y2] implies ( x1 = y1 & x2 = y2 ) )
assume A1: [x1,x2] = [y1,y2] ; :: thesis: ( x1 = y1 & x2 = y2 )

per cases ( y1 <> y2 or y1 = y2 ) ;

suppose A3: y1 <> y2 ; :: thesis: ( x1 = y1 & x2 = y2 )

then A4: {x1} <> {y1,y2} by Lx5;
then {x1} = {y1} by A1, Lx6;
then x1 in {y1} by TARSKI:def 1;
hence A5: x1 = y1 by TARSKI:def 1; :: thesis: x2 = y2
{y1,y2} = {x1,x2} by A1, A4, Lx6;
hence x2 = y2 by A3, A5, Lx6; :: thesis: verum

end;

suppose A6: y1 = y2 ; :: thesis: ( x1 = y1 & x2 = y2 )

then {{x1,x2},{x1}} = {{y1},{y1}} by A1, ENUMSET1:29
.= {{y1}} by ENUMSET1:29 ;
then {y1} = {x1,x2} by Lx4;
hence ( x1 = y1 & x2 = y2 ) by A6, Lx4; :: thesis: verum

end;

end;