let x1, x2, y1, y2 be object ; :: 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 A2: y1 <> y2 ; :: thesis: ( x1 = y1 & x2 = y2 )

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

end;

suppose A5: 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 Lm1;
hence ( x1 = y1 & x2 = y2 ) by A5, Lm1; :: thesis: verum

end;

end;