let x be object ; :: thesis: ( ex y, z being object st x = [y,z] implies ( x <> x `1 & x <> x `2 ) )
given y, z being object such that A1: x = [y,z] ; :: thesis: ( x <> x `1 & x <> x `2 )

now :: thesis: not y = x

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; :: thesis: x <> x `2

now :: thesis: not z = x

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; :: thesis: verum