x in X by Def1;
hence In (x,X) = x by Def7; :: thesis: verum