consider X being set such that
A1: for x being object holds
( x in X iff ( x = y or x = y ) ) by TARSKI_0:3;
take X ; :: thesis: for x being object holds
( x in X iff x = y )
thus for x being object holds
( x in X iff x = y ) by A1; :: thesis: verum