Let X, Tx and A be given.

Assume Htop: topology_on X Tx.

We will prove boundary_of X Tx A ⊆ closure_of X Tx A ∧ boundary_of X Tx A ⊆ closure_of X Tx (X ∖ A).

Apply andI to the current goal.

We will prove boundary_of X Tx A ⊆ closure_of X Tx A.

An exact proof term for the current goal is (binintersect_Subq_1 (closure_of X Tx A) (closure_of X Tx (X ∖ A))).

We will prove boundary_of X Tx A ⊆ closure_of X Tx (X ∖ A).

An exact proof term for the current goal is (binintersect_Subq_2 (closure_of X Tx A) (closure_of X Tx (X ∖ A))).

∎