Closeds of a ClosureOperator forms a CompleteLattice?

Stream: Is there code for X?

[Yijun Yuan]

You can see from here ClosureOperator.Closeds that Mathlib already knows how to define the set of closed elements of a closure operator. An important fact here is that the set of closed elements forms a complete lattice. To be more specific, we have:
/user_uploads/3121/R0UcfPkj_Hgel-b0eFE3RUby/_20250625105028.png
(P.S. This is a screenshot from Davey and Priestley's book Introduction to Lattices and Order)
This result enables us to perform various tasks, such as the Dedekind-MacNeille completion of a partially ordered set. However, I don't think this is already formalized in Mathlib, although the statement is quite short:

instance {α : Type} [PartialOrder α] (T : ClosureOperator (Set α)): CompleteLattice (ClosureOperator.Closeds T) := sorry