for H being ZF-formula
for x being Variable holds the_argument_of (Ex (x,H)) = All (x,('not' H)) by Th3;