Let X, A, B, S, Ts and WF be given.
Assume HWFdef: WF = {W0 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W0}.
Let W be given.
Assume HW: W ∈ WF.
We prove the intermediate claim HW': W ∈ {W0 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W0}.
rewrite the current goal using HWFdef (from right to left).
An exact proof term for the current goal is HW.
We prove the intermediate claim HWpred: ex32_8_WFpred X A B S Ts W.
An exact proof term for the current goal is (SepE2 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W HW').
An exact proof term for the current goal is (andEL (∃x : set, x ∈ S ∧ W = component_of S Ts x) (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W = order_interval X a b) HWpred).
∎