Let X, Tx, U and V be given.

Assume Htop: topology_on X Tx.

Assume HU: U ∈ Tx.

Assume HV: V ∈ Tx.

We will prove interior_of X Tx (U ∩ V) = U ∩ V.

We prove the intermediate claim HUV_open: U ∩ V ∈ Tx.

An exact proof term for the current goal is (lemma_intersection_two_open X Tx U V Htop HU HV).

An exact proof term for the current goal is (open_interior_eq X Tx (U ∩ V) Htop HUV_open).

∎