reconsider x = x as set by TARSKI:1;
x in X by A1;
hence x is Element of X by Def1; :: thesis: verum