reconsider xx = x as set by TARSKI:1;
not xx in xx ;
hence ( ( x in y implies a is object ) & ( x = y implies b is object ) & ( not x in y & not x = y implies c is object ) & ( for b₁ being object st x in y & x = y holds
( b₁ = a iff b₁ = b ) ) ) ; :: thesis: verum