let x, y be Variable; :: thesis: ( Var1 (x '=' y) = x & Var2 (x '=' y) = y )
x '=' y is being_equality ;
then x '=' y = (Var1 (x '=' y)) '=' (Var2 (x '=' y)) by ZF_LANG:36;
hence ( Var1 (x '=' y) = x & Var2 (x '=' y) = y ) by ZF_LANG:1; :: thesis: verum