let x, X be object ; :: thesis: [x,X] <> x
assume A1: [x,X] = x ; :: thesis: contradiction
reconsider x = x as set by TARSKI:1;
{x,X} in x by TARSKI:def 2, A1;
hence contradiction by TARSKI:def 2; :: thesis: verum