Let A and F be given.
Assume H1 H2.
Set Y to be the term {u ∈ A|∀X ∈ 𝒫 A, F X ⊆ X → u ∈ X} of type set.
We prove the intermediate claim L1: Y ∈ 𝒫 A.
Apply Sep_In_Power to the current goal.
We prove the intermediate claim L2: F Y ∈ 𝒫 A.
An exact proof term for the current goal is H1 Y L1.
We prove the intermediate claim L3: ∀X ∈ 𝒫 A, F X ⊆ X → Y ⊆ X.
Let X be given.
Assume HX: X ∈ 𝒫 A.
Assume H3: F X ⊆ X.
Let y be given.
Assume Hy: y ∈ Y.
An exact proof term for the current goal is SepE2 A (λu ⇒ ∀X ∈ 𝒫 A, F X ⊆ X → u ∈ X) y Hy X HX H3.
We prove the intermediate claim L4: F Y ⊆ Y.
Let u be given.
Assume H3: u ∈ F Y.
We will prove u ∈ Y.
Apply SepI to the current goal.
We will prove u ∈ A.
An exact proof term for the current goal is PowerE A (F Y) L2 u H3.
Let X be given.
Assume HX: X ∈ 𝒫 A.
Assume H4: F X ⊆ X.
We will prove u ∈ X.
We prove the intermediate claim L4a: Y ⊆ X.
An exact proof term for the current goal is L3 X HX H4.
We prove the intermediate claim L4b: F Y ⊆ F X.
An exact proof term for the current goal is H2 Y L1 X HX L4a.
We will prove u ∈ X.
Apply H4 to the current goal.
We will prove u ∈ F X.
Apply L4b to the current goal.
An exact proof term for the current goal is H3.
We prove the intermediate claim L5: F (F Y) ⊆ F Y.
An exact proof term for the current goal is H2 (F Y) L2 Y L1 L4.
We use Y to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is L1.
Apply set_ext to the current goal.
An exact proof term for the current goal is L4.
We will prove Y ⊆ F Y.
Apply L3 to the current goal.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is L5.
∎