reconsider y1 = y as Element of ;
reconsider x1 = x as Element of ;
[x1,y1] is Element of by Def2;
hence [x,y] is Element of ; :: thesis: verum