theorem :: ZF_LANG1:13

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