let H be ZF-formula; :: thesis: for x, y, z being Variable st x <> y holds
(H / x,y) / x,z = H / x,y
let x, y, z be Variable; :: thesis: ( x <> y implies (H / x,y) / x,z = H / x,y )
assume x <> y ; :: thesis: (H / x,y) / x,z = H / x,y
then not x in variables_in (H / x,y) by Th198;
hence (H / x,y) / x,z = H / x,y by Th196; :: thesis: verum