theorem Th1: :: ZF_LANG1:1

for x, y being Variable holds
( Var1 (x '=' y) = x & Var2 (x '=' y) = y )