Let U be given.
Assume HU: U ∈ top_abc_3.
We will prove U ∈ top_abc_2.
We prove the intermediate claim Ht2: top_abc_2 = 𝒫 abc_set.
Use reflexivity.
rewrite the current goal using Ht2 (from left to right).
Apply PowerI to the current goal.
Let x be given.
Assume Hx: x ∈ U.
We will prove x ∈ abc_set.
Apply (binunionE' (UPair Empty {a_elt}) {abc_set} U (x ∈ abc_set)) to the current goal.
Assume HU0: U ∈ UPair Empty {a_elt}.
Apply (UPairE U Empty {a_elt} HU0) to the current goal.
Assume HUeq: U = Empty.
We prove the intermediate claim HxEmpty: x ∈ Empty.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is (EmptyE x HxEmpty (x ∈ abc_set)).
Assume HUeq: U = {a_elt}.
We prove the intermediate claim HxSing: x ∈ {a_elt}.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is Hx.
We prove the intermediate claim Hxeq: x = a_elt.
An exact proof term for the current goal is (SingE a_elt x HxSing).
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair a_elt b_elt) {c_elt} a_elt (UPairI1 a_elt b_elt)).
Assume HU0: U ∈ {abc_set}.
We prove the intermediate claim HUeq: U = abc_set.
An exact proof term for the current goal is (SingE abc_set U HU0).
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is HU.
∎