Let X, T1, T2 and T3 be given.
Assume H12 H23.
We prove the intermediate claim H12pair: topology_on X T1 ∧ topology_on X T2.
An exact proof term for the current goal is (andEL (topology_on X T1 ∧ topology_on X T2) (T1 = T2) H12).
We prove the intermediate claim H12eq: T1 = T2.
An exact proof term for the current goal is (andER (topology_on X T1 ∧ topology_on X T2) (T1 = T2) H12).
We prove the intermediate claim HT1: topology_on X T1.
An exact proof term for the current goal is (andEL (topology_on X T1) (topology_on X T2) H12pair).
We prove the intermediate claim HT2: topology_on X T2.
An exact proof term for the current goal is (andER (topology_on X T1) (topology_on X T2) H12pair).
We prove the intermediate claim H23pair: topology_on X T2 ∧ topology_on X T3.
An exact proof term for the current goal is (andEL (topology_on X T2 ∧ topology_on X T3) (T2 = T3) H23).
We prove the intermediate claim H23eq: T2 = T3.
An exact proof term for the current goal is (andER (topology_on X T2 ∧ topology_on X T3) (T2 = T3) H23).
We prove the intermediate claim HT3: topology_on X T3.
An exact proof term for the current goal is (andER (topology_on X T2) (topology_on X T3) H23pair).
We will prove topology_on X T1 ∧ topology_on X T3 ∧ T1 = T3.
Apply and3I to the current goal.
An exact proof term for the current goal is HT1.
An exact proof term for the current goal is HT3.
rewrite the current goal using H12eq (from left to right).
rewrite the current goal using H23eq (from left to right).
Use reflexivity.
∎