Using the term once in the sentence does not fundamentally eliminate the circularity, which is actually a necessary condition of the definition, but to argue that presumes some knowledge of the act of definition.
The question you ask after is one about the nature of definition, so I'm going to formulate a response in regards to your question within the framework provided by Robinson's Definition in one of two good philosophical works devoted to the philosophy of definition itself. Inherent in Robinson's definition are some metaphilosophical positions that are, in and of themselves, dispubtable, such as the notion that speech acts that are definitional imperatives necessarily preclude the object proposition from have truth conditional, and so on. Therefore, you can certainly challenge the following account, but what you are asking about is what is the sense we should make of self-reference in definition, and starting with Robinson's analysis is a good start to find an answer that satisfies you.
Robinson offers a taxonomy of definition such that he divides the act of definition into two taxa, one related to linguistic activities, and one related to conceptual activities. In his estimation, the latter is called a real definition, which he laments should be called a definition at all. From pg. 149:
The inventors of the notion of definition, Socrates and Plato, were obviously thinking only of the definition of things and not at all of the definition of words. The search for the definition of piety in Plato's Eurthypro is certainly an inquiry about the thing piety, not about the word 'piety'.
(NB the use-mention distinction that presumes the syntax-semantic division.)
So, it is obvious, that if one dichotomizes in such a fashion, the the definition of infimum presented is not inherently an exercise in examining language, but of exploring in terms of necessity and sufficiency that which can be applied to a context to determine existential quantification. Thus, we have infimum as explanandum and the proposition as explanas. This should set off a red flag, because in an ordinary language conception, definiendum and definiens are the terminology used. Thus, we have an entire terminology of definition that minds the syntax-semantic distinction. This is important, because it draws a nuance necessary to give descriptivist insight into the purpose of the circularity inherent in impredicativity which seems to serve a pragmatic function of sorts despite it being logically tautological, an important Wittgensteinain theme on language use.
So what does Robinson mean when he uses the term real definition as opposed to word-thing definitions like lexical definitions (descriptivist acts of definition) and stipulative definitions (prescriptivist acts of definition)? Turns out, he argues there are no fewer than 12 distinctions in real definition that are occurring in positing a real definition. While it's beyond the scope of this post to flesh them out, the example you provided prima facie fits his stipulation of a speech act that is an analytical real definition. Onwards.
He describes definitions in this chapter as psychological speech acts, and not logical structures. To wit, he posits that there are real definitions which go to establish an abstraction exists (Real Definition as Abstraction, p.170) and then goes on to explain that the existential quantification of an abstraction then necessitates analysis and synthesis into a pre-established linguist framework. Thus, an analytical real definition takes a name of an abstraction, and then uses predicates to conjoin the name of the abstraction into the framework. Thus to use a set in its own definition is about taking a name of an abstraction, and then expressing criteria to clarify the language-game that goes into existential quantification. That's exactly what your example does. Thus, on the LHS of the analytical definition, we have the abstraction, but on the RHS of the definition, we have the abstraction in a model. (The mathematical logical characterization is mine, not his.)
So, a set defined in terms of itself needs to be tautological because it is a form of predication that is explicit about the relationships that are conjoined to the set itself. How could one predicate necessary conditions for existence without invoking the concept to begin with. And that's why it's explanandum and not definiendum. A analytical real definition explains a concept using semantic grounding, it doesn't offer a shallow syntactic substitution as in word-thing definitions.
A simpler way to explain it might be in the parlance of propositional calculus. A word-thing definition functions analogously to using logical equivalence to eliminate or reduce terms syntactically, where as using an analytical real definition would mean strictly introducing a predicated semantics which provides semantic grounding. In mathematics, this happens all of the time. We call it introducing rigor. So, the impredicativity of a definition of the infimum of a set in terms of the set itself occurs because prior to the introduction of the arithmetic constraint on a lower bound, there is an ambiguity of sorts that needs to be resolved. In fact, there's a name for this among us word mongerers, it's called a precising definition:
A precising definition is a definition that contracts or reduces the scope of the lexical definition of a term for a specific purpose by including additional criteria that narrow down the set of things meeting the definition
Thus, we have the infimum of a set naively and intuitively, and we have it rigorously using a metric space.
The moral of the story is that you are attempting to hide the circularity inherent in a precising definition by elliding over the term in your reformulation which works syntactically, but the circularity inherent is not a question of syntax, it is fundamentally bound to the semantics. So, I say no.