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 )

A2: now

assume A3: y1 <> y2 ; :: thesis: ( x1 = y1 & x2 = y2 )
then A4: {x1} <> {y1,y2} by Th9;
then {x1} = {y1} by A1, Th10;
hence A5: x1 = y1 by Th6; :: thesis: x2 = y2
{y1,y2} = {x1,x2} by A1, A4, Th10;
hence x2 = y2 by A3, A5, Th10; :: thesis: verum

end;

now

assume A6: y1 = y2 ; :: thesis: ( x1 = y1 & x2 = y2 )
then ( {{y1}} = {{y1},{y1}} & {{y1},{y1}} = {{x1,x2},{x1}} ) by A1, ENUMSET1:69;
then {y1} = {x1,x2} by Th8;
hence ( x1 = y1 & x2 = y2 ) by A6, Th8; :: thesis: verum

end;

hence ( x1 = y1 & x2 = y2 ) by A2; :: thesis: verum