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