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