基于前文，对前集（S，pre-set）、其成员关系（∈，membership），以及良创（Well-Founded）的定义，此文，分析（S, ∈）是良创的证明。

良创在lean中的定义

        也就是，对于（S, ∈）来说，任意前集都是基于其成员关系上可达的（Accessible）。同时，基于可达类型的定义，如下图

        即对于前集来说，当其所有元素也是基于成员关系可达的，那么其可达。这样，就会出现，要证明前集α₀可达，就要证明其所有的元素可达，如 α₁ ∈ α₀；要证明 α₁ ∈ α₀可达，就要证明，α₂ ∈ α₁可达，一直往下，有

... ∈ αₙ ∈ ... ∈ α₂ ∈ α₁ ∈ α₀

        此时，如果，对于任意前集 α₀，都存在对应的 ... ∈ αₙ ∈ ... ∈ α₂ ∈ α₁ ∈ α₀，那么，（S, ∈）就是良创的。

（S, ∈）良创的

        即，要证明，如下图， PSet 与 ∈ 是良创的

        通过证明，如果两前集 x, y 相等，那么前集 y 是可达的，即 mem_wf_aux 来证明 （PSet, ∈）是良创的。因此，有

        这里，看起来比较复杂，因为此证明中，使用 lean 的 tactic 机制。简单来说，这里的证明过程，是基于归纳法（induction）来证明。

        也就是，当 y 是空集是，（y, ∈）是可达的。

        当 y不是空集时，有 前集 x = y，那么，能证明 前集 x 的元素 x.Func a，其中，A = x.Func，a: α = x.Type，等于 前集 y 的元素 〈γ, C〉，那么，此时拥有的前提是，前集的元素可达，那么前集可达，也就是 mem_wf_aux的本身，即，mem_wf_aux H 为前集 y 的元素 〈γ, C〉可达的证明。

        换句话说，by 引出 tactic 的目的（goal）是 为了 证明 前集 y 的元素 〈γ, C〉，那在此证明的过程，可使用如下假设

        以及，mem_wf_aux 的本身。

        也就是说，mem_wf_aux 对于空集成立，mem_wf_aux 对只包含空集为元素的集合或空集也成立，对于更进一步的包含也成立，... 。

        综上所述，前集的良创性，说明了，前集是，通过对已有前集的包含，所创建出来的。