let x, X be set ; :: thesis: not [x,X] in X
assume A: [x,X] in X ; :: thesis: contradiction
B: X in {x,X} by TARSKI:def 2;
{x,X} in {{x,X},{x}} by TARSKI:def 2;
hence contradiction by A, B, XREGULAR:7; :: thesis: verum