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