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