---

{ [T:Type]. g1,g2,g3:LabeledGraph(T).  (g1  g2  g2  g3  g1  g3) }

{ Proof }

---

Definitions occuring in Statement :  lg-contains: g1  g2,  labeled-graph: LabeledGraph(T),  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  lg-contains: g1  g2,  exists: x:A. B[x],  member: t  T,  prop:
Lemmas :  lg-append_wf,  labeled-graph_wf,  lg-append_assoc

---

\mforall{}[T:Type].  \mforall{}g1,g2,g3:LabeledGraph(T).    (g1  \msubseteq{}  g2  {}\mRightarrow{}  g2  \msubseteq{}  g3  {}\mRightarrow{}  g1  \msubseteq{}  g3)


Date html generated: 2011_08_16-PM-06_36_45
Last ObjectModification: 2011_06_20-AM-01_56_25

Home Index