theorem :: ZF_LANG:8

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