src/ZF/Constructible/Rec_Separation.thy

 apply (intro FOL_reflections function_reflections
              rtran_closure_reflection composition_reflection)
 done
 
 
-subsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
+subsubsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
 
 lemma wellfounded_trancl_reflects:
   "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
                  w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
    \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i).