theorem :: ZF_LANG:35

for H being ZF-formula st H is atomic holds
( Var1 H = H . 2 & Var2 H = H . 3 ) by Def28, Def29;