In this blog post, the following definition of an "impredicative definition" is offered:

A definition is said to be impredicative if it defines an object E by means of a quantification over a domain of entities which includes E itself. An example: the standard definition of the infimum of a set X is impredicative. For we say that y = inf(X) if and only if y is a lower bound for X, and for any lower bound z of X, z ≤ y. And note that this definition quantifies over the lower bounds of X, one of which is the infimum itself (assuming there is one).

The point is made that some mathematicians think this type of definition is as bad as a circular definition. But how can that be? One just has to establish that there exists at least one lower bound for X to make this definition "good". Two things can happen: either a lower bound does not exist, and then there is no infimum because there is no lower bound, or there is at least one lower bound, and then the definition of infimum is operative, and doesn't seem circular to me. Is the concern that this definition hides a premise that one needs to establish the existence of at least one lower bound first? This would seem trivial to resolve, rather than rejecting the definition wholesale as "impredicative".

If that definition was changed to:

Given a set X, if (1) there exists lower bounds of X, (2) lower bounds can be ordered and (3) y is a lower bound for X such that (4) for any lower bound z of X, z ≤ y, then y is called inf(X)

would it sill be impredicative? The various existence requirements are clearly stipulated in the premises, and only if they are all met, can we call one of the lower bounds the "infimum". But up to the conclusion the existence of the "infimum" itself is not assumed, so there seems to be no circularity.