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 )
X: ( [y,z] `1 = y & [y,z] `2 = z ) ;

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