theorem Th2: :: ZF_LANG1:2

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