---

Step * of Lemma lg-contains_antisymmetry

∀[T:Type]. ∀[g1,g2:LabeledGraph(T)].  (g1 = g2 ∈ LabeledGraph(T)) supposing (g2 ⊆ g1 and g1 ⊆ g2)
BY
{ (Unfold `lg-contains` 0
   THEN Auto
   THEN ExRepD
   THEN (Assert (lg-size(ga) = 0 ∈ ℤ) ∧ (lg-size(gb) = 0 ∈ ℤ) BY
               (∀h:hyp. ((ApFunToHypEquands `g' ⌜lg-size(g)⌝ ⌜ℤ⌝ h⋅ THENA Auto)
                         THEN (RWW "lg-size-append" (-1) THENA Auto)
                         ) 
                THEN Auto'
                ))) }

1
1. T : Type
2. g1 : LabeledGraph(T)
3. g2 : LabeledGraph(T)
4. g3 : LabeledGraph(T)
5. g4 : LabeledGraph(T)
6. g2 = lg-append(g3;lg-append(g1;g4)) ∈ LabeledGraph(T)
7. ga : LabeledGraph(T)
8. gb : LabeledGraph(T)
9. g1 = lg-append(ga;lg-append(g2;gb)) ∈ LabeledGraph(T)
10. (lg-size(ga) = 0 ∈ ℤ) ∧ (lg-size(gb) = 0 ∈ ℤ)
⊢ g1 = g2 ∈ LabeledGraph(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g1,g2:LabeledGraph(T)].    (g1  =  g2)  supposing  (g2  \msubseteq{}  g1  and  g1  \msubseteq{}  g2)


By

---

Latex:
(Unfold  `lg-contains`  0
  THEN  Auto
  THEN  ExRepD
  THEN  (Assert  (lg-size(ga)  =  0)  \mwedge{}  (lg-size(gb)  =  0)  BY
                          (\mforall{}h:hyp.  ((ApFunToHypEquands  `g'  \mkleeneopen{}lg-size(g)\mkleeneclose{}  \mkleeneopen{}\mBbbZ{}\mkleeneclose{}  h\mcdot{}  THENA  Auto)
                                              THEN  (RWW  "lg-size-append"  (-1)  THENA  Auto)
                                              ) 
                            THEN  Auto'
                            )))

---

Home Index