Step
*
of Lemma
not-added-name
∀[I:fset(ℕ)]. ∀[i:ℕ]. ∀[x:names(I+i)]. x ∈ names(I) supposing x ≠ i
BY
{ (Auto THEN DVar `x' THEN (RWO "fset-member-add-name" (-2)⋅ THENA Auto) THEN D -2 THEN Auto) }
Latex:
Latex:
\mforall{}[I:fset(\mBbbN{})]. \mforall{}[i:\mBbbN{}]. \mforall{}[x:names(I+i)]. x \mmember{} names(I) supposing x \mneq{} i
By
Latex:
(Auto THEN DVar `x' THEN (RWO "fset-member-add-name" (-2)\mcdot{} THENA Auto) THEN D -2 THEN Auto)
Home
Index