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