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