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 )

now

assume y = x ; :: thesis: contradiction
then {{y,z},{y}} in {y} by A1, TARSKI:def 1;
hence contradiction by TARSKI:def 2; :: 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} by A1, TARSKI:def 2;
hence contradiction by TARSKI:def 2; :: thesis: verum

end;

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