let x be object ; :: thesis: for X being set holds not [x,X] in X
let X be set ; :: thesis: not [x,X] in X
A1: X in {x,X} by TARSKI:def 2;
{x,X} in {{x,X},{x}} by TARSKI:def 2;
hence not [x,X] in X by A1, XREGULAR:7; :: thesis: verum