theorem :: ZF_LANG:7

for x, y being Variable
for H being ZF-formula holds
( All (x,y,H) = All (x,(All (y,H))) & Ex (x,y,H) = Ex (x,(Ex (y,H))) ) ;