theorem :: ZF_LANG1:18

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