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