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