`∀k:ℕ`
`  ∀[T:Type]`
`    (T ~ ℕk`
`    `` (∀[R:bag(T) ⟶ bag(T) ⟶ ℙ]`
`          ((∀as,bs:bag(T).  Dec(R[as;bs]))`
`          `` Order(bag(T);as,bs.R[as;bs])`
`          `` bag-admissable(T;as,bs.R[as;bs])`
`          `` WellFnd{i}(bag(T);as,bs.R[as;bs] ∧ (¬(as = bs ∈ bag(T)))))))`

Proof

Definitions occuring in Statement :  bag-admissable: `bag-admissable(T;as,bs.R[as; bs])` bag: `bag(T)` equipollent: `A ~ B` order: `Order(T;x,y.R[x; y])` int_seg: `{i..j-}` nat: `ℕ` wellfounded: `WellFnd{i}(A;x,y.R[x; y])` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` and: `P ∧ Q` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` not: `¬A` false: `False` so_lambda: `λ2x.t[x]` so_apply: `x[s]` nat: `ℕ` trans: `Trans(T;x,y.E[x; y])` cand: `A c∧ B` guard: `{T}` order: `Order(T;x,y.R[x; y])` anti_sym: `AntiSym(T;x,y.R[x; y])`
Lemmas referenced :  bag-ordering-wellfounded bag_wf not_wf equal_wf sub-bag_wf bag-admissable_wf order_wf all_wf decidable_wf equipollent_wf int_seg_wf nat_wf and_wf decidable__equal_equipollent decidable__cand decidable__not decidable__equal_bag sub-bag-admissable
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination independent_functionElimination hypothesis sqequalRule lambdaEquality productEquality applyEquality functionExtensionality cumulativity universeEquality voidElimination because_Cache functionEquality natural_numberEquality setElimination rename productElimination independent_pairFormation hyp_replacement equalitySymmetry dependent_set_memberEquality setEquality isect_memberEquality

Latex:
\mforall{}k:\mBbbN{}
\mforall{}[T:Type]
(T  \msim{}  \mBbbN{}k
{}\mRightarrow{}  (\mforall{}[R:bag(T)  {}\mrightarrow{}  bag(T)  {}\mrightarrow{}  \mBbbP{}]
((\mforall{}as,bs:bag(T).    Dec(R[as;bs]))
{}\mRightarrow{}  Order(bag(T);as,bs.R[as;bs])