let x, y be Variable; :: thesis: Free (x 'in' y) = {x,y}
( x 'in' y is being_membership & Var1 (x 'in' y) = x & Var2 (x 'in' y) = y ) by Th2, ZF_LANG:16;
hence Free (x 'in' y) = {x,y} by ZF_MODEL:1; :: thesis: verum