theorem :: ZF_LANG:2

for x, y, z, t being Variable st x 'in' y = z 'in' t holds
( x = z & y = t )