---

Step * of Lemma sub-bag_antisymmetry

∀[T:Type]. ∀[as,bs:bag(T)].  (as = bs ∈ bag(T)) supposing (sub-bag(T;as;bs) and sub-bag(T;bs;as))
BY
{ ((Unfold `sub-bag` 0 THEN Auto)
   THEN ExRepD
   THEN RepeatFor 2 ((DupHyp (-3)
                      THEN (ApFunToHypEquands `B' ⌜#(B)⌝ ⌜ℤ⌝ (-1)⋅ THENA Auto)
                      THEN (RWO "bag-size-append" (-1) THENA Auto)))) }

1
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. c1 : bag(T)
5. as = (bs + c1) ∈ bag(T)
6. cs : bag(T)
7. bs = (as + cs) ∈ bag(T)
8. as = (bs + c1) ∈ bag(T)
9. #(as) = (#(bs) + #(c1)) ∈ ℤ
10. bs = (as + cs) ∈ bag(T)
11. #(bs) = (#(as) + #(cs)) ∈ ℤ
⊢ as = bs ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].    (as  =  bs)  supposing  (sub-bag(T;as;bs)  and  sub-bag(T;bs;as))


By

---

Latex:
((Unfold  `sub-bag`  0  THEN  Auto)
  THEN  ExRepD
  THEN  RepeatFor  2  ((DupHyp  (-3)
                                        THEN  (ApFunToHypEquands  `B'  \mkleeneopen{}\#(B)\mkleeneclose{}  \mkleeneopen{}\mBbbZ{}\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                                        THEN  (RWO  "bag-size-append"  (-1)  THENA  Auto))))

---

Home Index