[x,y] is Element of by Def1;
hence [x,y] is Element of ; :: thesis: verum