let x, y be Variable; :: thesis: ( Var1 (x 'in' y) = x & Var2 (x 'in' y) = y )
x 'in' y is being_membership ;
then x 'in' y = (Var1 (x 'in' y)) 'in' (Var2 (x 'in' y)) by ZF_LANG:37;
hence ( Var1 (x 'in' y) = x & Var2 (x 'in' y) = y ) by ZF_LANG:2; :: thesis: verum