let x be set ; :: thesis: ( ex y, z being set st x = [y,z] implies ( x <> x `1 & x <> x `2 ) )
given y, z being set such that A1: x = [y,z] ; :: thesis: ( x <> x `1 & x <> x `2 )
A2: x = {{y,z},{y}} by A1, TARSKI:def 5;

now

assume y = x ; :: thesis: contradiction
then ( {{y,z},{y}} in {y} & {y} in {{y,z},{y}} ) by A2, TARSKI:def 1, TARSKI:def 2;
hence contradiction ; :: thesis: verum

end;

hence x <> x `1 by A1, Def1; :: thesis: x <> x `2

now

assume z = x ; :: thesis: contradiction
then ( {{y,z},{y}} in {y,z} & {y,z} in {{y,z},{y}} ) by A2, TARSKI:def 2;
hence contradiction ; :: thesis: verum

end;

hence x <> x `2 by A1, Def2; :: thesis: verum