Let X, Tx, A and B be given.

Assume HTx: topology_on X Tx.

Assume HAsubX: A ⊆ X.

Assume Hclsub: closure_of X Tx A ⊆ B.

An exact proof term for the current goal is (Subq_tra A (closure_of X Tx A) B (subset_of_closure X Tx A HTx HAsubX) Hclsub).

∎